:: MSUALG_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let I be non empty set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
let i be Element of I;
:: original: .
redefine func F . i -> Function of A . i,B . i;
coherence
F . i is Function of A . i,B . i by PBOOLE:def 18;
end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1,the Sorts of U2;
end;

definition
let I be set ;
let A be ManySortedSet of I;
func id A -> ManySortedFunction of A,A means :Def1: :: MSUALG_3:def 1
for i being set st i in I holds
it . i = id (A . i);
existence
ex b1 being ManySortedFunction of A,A st
for i being set st i in I holds
b1 . i = id (A . i)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of A,A st ( for i being set st i in I holds
b1 . i = id (A . i) ) & ( for i being set st i in I holds
b2 . i = id (A . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines id MSUALG_3:def 1 :
for I being set
for A being ManySortedSet of I
for b3 being ManySortedFunction of A,A holds
( b3 = id A iff for i being set st i in I holds
b3 . i = id (A . i) );

definition
let IT be Function;
attr IT is "1-1" means :Def2: :: MSUALG_3:def 2
for i being set
for f being Function st i in dom IT & IT . i = f holds
f is one-to-one;
end;

:: deftheorem Def2 defines "1-1" MSUALG_3:def 2 :
for IT being Function holds
( IT is "1-1" iff for i being set
for f being Function st i in dom IT & IT . i = f holds
f is one-to-one );

registration
let I be set ;
cluster "1-1" ManySortedSet of I;
existence
ex b1 being ManySortedFunction of I st b1 is "1-1"
proof end;
end;

theorem Th1: :: MSUALG_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for F being ManySortedFunction of I holds
( F is "1-1" iff for i being set st i in I holds
F . i is one-to-one )
proof end;

definition
let I be set ;
let A, B be ManySortedSet of I;
let IT be ManySortedFunction of A,B;
attr IT is "onto" means :Def3: :: MSUALG_3:def 3
for i being set st i in I holds
rng (IT . i) = B . i;
end;

:: deftheorem Def3 defines "onto" MSUALG_3:def 3 :
for I being set
for A, B being ManySortedSet of I
for IT being ManySortedFunction of A,B holds
( IT is "onto" iff for i being set st i in I holds
rng (IT . i) = B . i );

theorem Th2: :: MSUALG_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )
proof end;

definition
let I be set ;
let A be ManySortedSet of I;
let B, C be V3 ManySortedSet of I;
let F be ManySortedFunction of A,B;
let G be ManySortedFunction of B,C;
:: original: **
redefine func G ** F -> ManySortedFunction of A,C;
coherence
G ** F is ManySortedFunction of A,C
proof end;
end;

theorem :: MSUALG_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds F ** (id A) = F
proof end;

theorem Th4: :: MSUALG_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds (id B) ** F = F
proof end;

definition
let I be set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
assume A1: ( F is "1-1" & F is "onto" ) ;
canceled;
func F "" -> ManySortedFunction of B,A means :Def5: :: MSUALG_3:def 5
for i being set st i in I holds
it . i = (F . i) " ;
existence
ex b1 being ManySortedFunction of B,A st
for i being set st i in I holds
b1 . i = (F . i) "
proof end;
uniqueness
for b1, b2 being ManySortedFunction of B,A st ( for i being set st i in I holds
b1 . i = (F . i) " ) & ( for i being set st i in I holds
b2 . i = (F . i) " ) holds
b1 = b2
proof end;
end;

:: deftheorem MSUALG_3:def 4 :
canceled;

:: deftheorem Def5 defines "" MSUALG_3:def 5 :
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
for b5 being ManySortedFunction of B,A holds
( b5 = F "" iff for i being set st i in I holds
b5 . i = (F . i) " );

theorem Th5: :: MSUALG_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being V3 ManySortedSet of I
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
proof end;

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
let o be OperSymbol of S;
cluster Args o,U1 -> functional ;
coherence
Args o,U1 is functional
proof end;
end;

theorem Th6: :: MSUALG_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra of S
for x being Function st x in Args o,U1 holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom (the Sorts of U1 * (the_arity_of o)) holds
x . y in (the Sorts of U1 * (the_arity_of o)) . y ) )
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
let o be OperSymbol of S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args o,U1;
assume that
A1: Args o,U1 <> {} and
A2: Args o,U2 <> {} ;
canceled;
func F # x -> Element of Args o,U2 equals :Def7: :: MSUALG_3:def 7
(Frege (F * (the_arity_of o))) . x;
coherence
(Frege (F * (the_arity_of o))) . x is Element of Args o,U2
proof end;
correctness
;
end;

:: deftheorem MSUALG_3:def 6 :
canceled;

:: deftheorem Def7 defines # MSUALG_3:def 7 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1 st Args o,U1 <> {} & Args o,U2 <> {} holds
F # x = (Frege (F * (the_arity_of o))) . x;

Lm1: now
let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )
let U1, U2 be MSAlgebra of S; :: thesis: for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )
let o be OperSymbol of S; :: thesis: for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )
let F be ManySortedFunction of U1,U2; :: thesis: for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )
let x be Element of Args o,U1; :: thesis: for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )
let f, u be Function; :: thesis: ( x = f & x in Args o,U1 & u in Args o,U2 implies ( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) )
assume A1: ( x = f & x in Args o,U1 & u in Args o,U2 ) ; :: thesis: ( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )
A2: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then A3: rng (the_arity_of o) c= dom the Sorts of U1 by PBOOLE:def 3;
A4: ( Args o,U1 = product (the Sorts of U1 * (the_arity_of o)) & Args o,U2 = product (the Sorts of U2 * (the_arity_of o)) ) by PRALG_2:10;
then A5: dom f = dom (the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:18
.= dom (the_arity_of o) by A3, RELAT_1:46 ;
A6: rng (the_arity_of o) c= dom the Sorts of U2 by A2, PBOOLE:def 3;
A7: dom u = dom (the Sorts of U2 * (the_arity_of o)) by A1, A4, CARD_3:18;
then A8: dom u = dom (the_arity_of o) by A6, RELAT_1:46;
A9: dom (the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) c= dom (the Sorts of U1 * (the_arity_of o))
let e be set ; :: thesis: ( e in dom (the Sorts of U1 * (the_arity_of o)) implies e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) )
assume A10: e in dom (the Sorts of U1 * (the_arity_of o)) ; :: thesis: e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
then A11: e in dom (the_arity_of o) by FUNCT_1:21;
(the_arity_of o) . e in dom the Sorts of U1 by A10, FUNCT_1:21;
then (the_arity_of o) . e in the carrier of S by PBOOLE:def 3;
then (the_arity_of o) . e in dom F by PBOOLE:def 3;
then A12: e in dom (F * (the_arity_of o)) by A11, FUNCT_1:21;
(F * (the_arity_of o)) . e is Function ;
hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A12, FUNCT_6:28; :: thesis: verum
end;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) or e in dom (the Sorts of U1 * (the_arity_of o)) )
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; :: thesis: e in dom (the Sorts of U1 * (the_arity_of o))
then e in dom (F * (the_arity_of o)) by FUNCT_6:28;
then A13: e in dom (the_arity_of o) by FUNCT_1:21;
then (the_arity_of o) . e in the carrier of S by FINSEQ_2:13;
then (the_arity_of o) . e in dom the Sorts of U1 by PBOOLE:def 3;
hence e in dom (the Sorts of U1 * (the_arity_of o)) by A13, FUNCT_1:21; :: thesis: verum
end;
now
let e be set ; :: thesis: ( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies (the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) )
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; :: thesis: (the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)
then e in dom (F * (the_arity_of o)) by FUNCT_6:28;
then A14: e in dom (the_arity_of o) by FUNCT_1:21;
then (the_arity_of o) . e in the carrier of S by FINSEQ_2:13;
then reconsider Foe = F . ((the_arity_of o) . e) as Function of the Sorts of U1 . ((the_arity_of o) . e),the Sorts of U2 . ((the_arity_of o) . e) by PBOOLE:def 18;
A15: ( (the Sorts of U1 * (the_arity_of o)) . e = the Sorts of U1 . ((the_arity_of o) . e) & (the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) ) by A14, FUNCT_1:23;
(the Sorts of U2 * (the_arity_of o)) . e in rng (the Sorts of U2 * (the_arity_of o)) by A7, A8, A14, FUNCT_1:def 5;
then (the Sorts of U2 * (the_arity_of o)) . e <> {} by A1, A4, CARD_3:37;
hence (the Sorts of U1 * (the_arity_of o)) . e = dom Foe by A15, FUNCT_2:def 1
.= proj1 Foe by FUNCT_5:21
.= proj1 ((F * (the_arity_of o)) . e) by A14, FUNCT_1:23 ;
:: thesis: verum
end;
then A16: the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o)) by A9, FUNCT_6:def 2;
hereby :: thesis: ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x )
assume u = F # x ; :: thesis: for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n)
then A17: u = (Frege (F * (the_arity_of o))) . x by A1, Def7;
let n be Nat; :: thesis: ( n in dom f implies u . n = (F . ((the_arity_of o) /. n)) . (f . n) )
assume A18: n in dom f ; :: thesis: u . n = (F . ((the_arity_of o) /. n)) . (f . n)
then (the_arity_of o) . n in the carrier of S by A5, FINSEQ_2:13;
then (the_arity_of o) . n in dom F by PBOOLE:def 3;
then A19: n in dom (F * (the_arity_of o)) by A5, A18, FUNCT_1:21;
then A20: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:22
.= F . ((the_arity_of o) /. n) by A5, A18, FINSEQ_4:def 4 ;
thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A4, A16, A17, PRALG_2:def 8
.= (F . ((the_arity_of o) /. n)) . (f . n) by A19, A20, PRALG_1:def 17 ; :: thesis: verum
end;
assume A21: for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; :: thesis: u = F # x
A22: rng (the_arity_of o) c= dom F by A2, PBOOLE:def 3;
F # x is Element of product (the Sorts of U2 * (the_arity_of o)) by PRALG_2:10;
then reconsider g = F # x as Function ;
A23: F # x = (Frege (F * (the_arity_of o))) . x by A1, Def7;
then F # x = (F * (the_arity_of o)) .. f by A1, A4, A16, PRALG_2:def 8;
then A24: dom g = dom (F * (the_arity_of o)) by PRALG_1:def 17
.= dom f by A5, A22, RELAT_1:46 ;
now
let e be set ; :: thesis: ( e in dom f implies u . e = g . e )
assume A25: e in dom f ; :: thesis: u . e = g . e
then reconsider n = e as Nat by A5;
(the_arity_of o) . n in the carrier of S by A5, A25, FINSEQ_2:13;
then (the_arity_of o) . n in dom F by PBOOLE:def 3;
then A26: n in dom (F * (the_arity_of o)) by A5, A25, FUNCT_1:21;
then A27: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:22
.= F . ((the_arity_of o) /. n) by A5, A25, FINSEQ_4:def 4 ;
thus u . e = (F . ((the_arity_of o) /. n)) . (f . n) by A21, A25
.= ((F * (the_arity_of o)) .. f) . n by A26, A27, PRALG_1:def 17
.= g . e by A1, A4, A16, A23, PRALG_2:def 8 ; :: thesis: verum
end;
hence u = F # x by A5, A8, A24, FUNCT_1:9; :: thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra of S;
let o be OperSymbol of S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args o,U1;
:: original: #
redefine func F # x -> Element of Args o,U2 means :Def8: :: MSUALG_3:def 8
for n being Nat st n in dom x holds
it . n = (F . ((the_arity_of o) /. n)) . (x . n);
coherence
F # x is Element of Args o,U2 ;
compatibility
for b1 being Element of Args o,U2 holds
( b1 = F # x iff for n being Nat st n in dom x holds
b1 . n = (F . ((the_arity_of o) /. n)) . (x . n) ) by Lm1;
end;

:: deftheorem Def8 defines # MSUALG_3:def 8 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for b7 being Element of Args o,U2 holds
( b7 = F # x iff for n being Nat st n in dom x holds
b7 . n = (F . ((the_arity_of o) /. n)) . (x . n) );

theorem Th7: :: MSUALG_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra of S st Args o,U1 <> {} holds
for x being Element of Args o,U1 holds x = (id the Sorts of U1) # x
proof end;

theorem Th8: :: MSUALG_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra of S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args o,U1 holds (H2 ** H1) # x = H2 # (H1 # x)
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
let F be ManySortedFunction of U1,U2;
pred F is_homomorphism U1,U2 means :Def9: :: MSUALG_3:def 9
for o being OperSymbol of S st Args o,U1 <> {} holds
for x being Element of Args o,U1 holds (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x);
end;

:: deftheorem Def9 defines is_homomorphism MSUALG_3:def 9 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_homomorphism U1,U2 iff for o being OperSymbol of S st Args o,U1 <> {} holds
for x being Element of Args o,U1 holds (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x) );

theorem Th9: :: MSUALG_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being MSAlgebra of S holds id the Sorts of U1 is_homomorphism U1,U1
proof end;

theorem Th10: :: MSUALG_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra of S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
let F be ManySortedFunction of U1,U2;
pred F is_epimorphism U1,U2 means :Def10: :: MSUALG_3:def 10
( F is_homomorphism U1,U2 & F is "onto" );
end;

:: deftheorem Def10 defines is_epimorphism MSUALG_3:def 10 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_epimorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" ) );

theorem Th11: :: MSUALG_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
let F be ManySortedFunction of U1,U2;
pred F is_monomorphism U1,U2 means :Def11: :: MSUALG_3:def 11
( F is_homomorphism U1,U2 & F is "1-1" );
end;

:: deftheorem Def11 defines is_monomorphism MSUALG_3:def 11 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_monomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "1-1" ) );

theorem Th12: :: MSUALG_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
let F be ManySortedFunction of U1,U2;
pred F is_isomorphism U1,U2 means :Def12: :: MSUALG_3:def 12
( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 );
end;

:: deftheorem Def12 defines is_isomorphism MSUALG_3:def 12 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) );

theorem Th13: :: MSUALG_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )
proof end;

Lm2: for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1
proof end;

theorem Th14: :: MSUALG_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
proof end;

theorem Th15: :: MSUALG_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra of S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
pred U1,U2 are_isomorphic means :Def13: :: MSUALG_3:def 13
 ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;
end;

:: deftheorem Def13 defines are_isomorphic MSUALG_3:def 13 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S holds
( U1,U2 are_isomorphic iff ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2 );

theorem Th16: :: MSUALG_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being MSAlgebra of S holds
( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra of S;
:: original: are_isomorphic
redefine pred U1,U2 are_isomorphic ;
reflexivity
for U1 being MSAlgebra of S holds U1,U1 are_isomorphic by Th16;
end;

theorem :: MSUALG_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic
proof end;

theorem :: MSUALG_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra of S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra of S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 ;
func Image F -> strict non-empty MSSubAlgebra of U2 means :Def14: :: MSUALG_3:def 14
the Sorts of it = F .:.: the Sorts of U1;
existence
ex b1 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1
proof end;
uniqueness
for b1, b2 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1 & the Sorts of b2 = F .:.: the Sorts of U1 holds
b1 = b2 by MSUALG_2:10;
end;

:: deftheorem Def14 defines Image MSUALG_3:def 14 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b5 being strict non-empty MSSubAlgebra of U2 holds
( b5 = Image F iff the Sorts of b5 = F .:.: the Sorts of U1 );

theorem :: MSUALG_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for U2 being strict non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = U2 )
proof end;

Lm3: for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
proof end;

theorem Th20: :: MSUALG_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
proof end;

theorem :: MSUALG_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F )
proof end;

Lm4: for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for U3 being non-empty MSSubAlgebra of U2
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
proof end;

theorem Th22: :: MSUALG_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for U2 being non-empty MSSubAlgebra of U1
for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1
proof end;

theorem :: MSUALG_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
proof end;

theorem :: MSUALG_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( u = F # x iff for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) by Lm1;