:: MSUALG_3 semantic presentation

definition
let c1 be non empty set ;
let c2, c3 be ManySortedSet of c1;
let c4 be ManySortedFunction of c2,c3;
let c5 be Element of c1;
redefine func . as c4 . c5 -> Function of a2 . a5,a3 . a5;
coherence
c4 . c5 is Function of c2 . c5,c3 . c5 by PBOOLE:def 18;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
mode ManySortedFunction of a2,a3 is ManySortedFunction of the Sorts of a2,the Sorts of a3;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
func id c2 -> ManySortedFunction of a2,a2 means :Def1: :: MSUALG_3:def 1
for b1 being set st b1 in a1 holds
a3 . b1 = id (a2 . b1);
existence
ex b1 being ManySortedFunction of c2,c2 st
for b2 being set st b2 in c1 holds
b1 . b2 = id (c2 . b2)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of c2,c2 st ( for b3 being set st b3 in c1 holds
b1 . b3 = id (c2 . b3) ) & ( for b3 being set st b3 in c1 holds
b2 . b3 = id (c2 . b3) ) holds
b1 = b2
proof end;
end;

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

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

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

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

theorem Th1: :: MSUALG_3:1
for b1 being set
for b2 being ManySortedFunction of b1 holds
( b2 is "1-1" iff for b3 being set st b3 in b1 holds
b2 . b3 is one-to-one )
proof end;

definition
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
let c4 be ManySortedFunction of c2,c3;
attr a4 is "onto" means :Def3: :: MSUALG_3:def 3
for b1 being set st b1 in a1 holds
rng (a4 . b1) = a3 . b1;
end;

:: deftheorem Def3 defines "onto" MSUALG_3:def 3 :
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is "onto" iff for b5 being set st b5 in b1 holds
rng (b4 . b5) = b3 . b5 );

theorem Th2: :: MSUALG_3:2
for b1 being set
for b2, b3, b4 being ManySortedSet of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 holds
( dom (b6 ** b5) = b1 & ( for b7 being set st b7 in b1 holds
(b6 ** b5) . b7 = (b6 . b7) * (b5 . b7) ) )
proof end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3, c4 be V3 ManySortedSet of c1;
let c5 be ManySortedFunction of c2,c3;
let c6 be ManySortedFunction of c3,c4;
redefine func ** as c6 ** c5 -> ManySortedFunction of a2,a4;
coherence
c6 ** c5 is ManySortedFunction of c2,c4
proof end;
end;

theorem Th3: :: MSUALG_3:3
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 holds b4 ** (id b2) = b4
proof end;

theorem Th4: :: MSUALG_3:4
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 holds (id b3) ** b4 = b4
proof end;

definition
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
let c4 be ManySortedFunction of c2,c3;
assume E7: ( c4 is "1-1" & c4 is "onto" ) ;
canceled;
func c4 "" -> ManySortedFunction of a3,a2 means :Def5: :: MSUALG_3:def 5
for b1 being set st b1 in a1 holds
a5 . b1 = (a4 . b1) " ;
existence
ex b1 being ManySortedFunction of c3,c2 st
for b2 being set st b2 in c1 holds
b1 . b2 = (c4 . b2) "
proof end;
uniqueness
for b1, b2 being ManySortedFunction of c3,c2 st ( for b3 being set st b3 in c1 holds
b1 . b3 = (c4 . b3) " ) & ( for b3 being set st b3 in c1 holds
b2 . b3 = (c4 . b3) " ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 MSUALG_3:def 4 :
canceled;

:: deftheorem Def5 defines "" MSUALG_3:def 5 :
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 st b4 is "1-1" & b4 is "onto" holds
for b5 being ManySortedFunction of b3,b2 holds
( b5 = b4 "" iff for b6 being set st b6 in b1 holds
b5 . b6 = (b4 . b6) " );

theorem Th5: :: MSUALG_3:5
for b1 being set
for b2, b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedFunction of b3,b2 st b4 is "1-1" & b4 is "onto" & b5 = b4 "" holds
( b4 ** b5 = id b3 & b5 ** b4 = id b2 )
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be OperSymbol of c1;
cluster Args a3,a2 -> functional ;
coherence
Args c3,c2 is functional
proof end;
end;

theorem Th6: :: MSUALG_3:6
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being MSAlgebra of b1
for b4 being Function st b4 in Args b2,b3 holds
( dom b4 = dom (the_arity_of b2) & ( for b5 being set st b5 in dom (the Sorts of b3 * (the_arity_of b2)) holds
b4 . b5 in (the Sorts of b3 * (the_arity_of b2)) . b5 ) )
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
let c4 be OperSymbol of c1;
let c5 be ManySortedFunction of c2,c3;
let c6 be Element of Args c4,c2;
assume that
E10: Args c4,c2 <> {} and
E11: Args c4,c3 <> {} ;
canceled;
func c5 # c6 -> Element of Args a4,a3 equals :Def7: :: MSUALG_3:def 7
(Frege (a5 * (the_arity_of a4))) . a6;
coherence
(Frege (c5 * (the_arity_of c4))) . c6 is Element of Args c4,c3
proof end;
correctness
;
end;

:: deftheorem Def6 MSUALG_3:def 6 :
canceled;

:: deftheorem Def7 defines # MSUALG_3:def 7 :
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being OperSymbol of b1
for b5 being ManySortedFunction of b2,b3
for b6 being Element of Args b4,b2 st Args b4,b2 <> {} & Args b4,b3 <> {} holds
b5 # b6 = (Frege (b5 * (the_arity_of b4))) . b6;

E11: now
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
let c4 be OperSymbol of c1;
let c5 be ManySortedFunction of c2,c3;
let c6 be Element of Args c4,c2;
let c7, c8 be Function;
assume E12: ( c6 = c7 & c6 in Args c4,c2 & c8 in Args c4,c3 ) ;
E13: rng (the_arity_of c4) c= the carrier of c1 by FINSEQ_1:def 4;
then E14: rng (the_arity_of c4) c= dom the Sorts of c2 by PBOOLE:def 3;
E15: ( Args c4,c2 = product (the Sorts of c2 * (the_arity_of c4)) & Args c4,c3 = product (the Sorts of c3 * (the_arity_of c4)) ) by PRALG_2:10;
then E16: dom c7 = dom (the Sorts of c2 * (the_arity_of c4)) by E12, CARD_3:18
.= dom (the_arity_of c4) by E14, RELAT_1:46 ;
E17: rng (the_arity_of c4) c= dom the Sorts of c3 by E13, PBOOLE:def 3;
E18: dom c8 = dom (the Sorts of c3 * (the_arity_of c4)) by E12, E15, CARD_3:18;
then E19: dom c8 = dom (the_arity_of c4) by E17, RELAT_1:46;
E20: dom (the Sorts of c2 * (the_arity_of c4)) = (c5 * (the_arity_of c4)) " (SubFuncs (rng (c5 * (the_arity_of c4))))
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c9 be set ;
assume E21: c9 in dom (the Sorts of c2 * (the_arity_of c4)) ;
then E22: c9 in dom (the_arity_of c4) by FUNCT_1:21;
(the_arity_of c4) . c9 in dom the Sorts of c2 by E21, FUNCT_1:21;
then (the_arity_of c4) . c9 in the carrier of c1 by PBOOLE:def 3;
then (the_arity_of c4) . c9 in dom c5 by PBOOLE:def 3;
then E23: c9 in dom (c5 * (the_arity_of c4)) by E22, FUNCT_1:21;
(c5 * (the_arity_of c4)) . c9 is Function ;
hence c9 in (c5 * (the_arity_of c4)) " (SubFuncs (rng (c5 * (the_arity_of c4)))) by E23, FUNCT_6:28;
end;
let c9 be set ; :: according to TARSKI:def 3
assume c9 in (c5 * (the_arity_of c4)) " (SubFuncs (rng (c5 * (the_arity_of c4)))) ;
then c9 in dom (c5 * (the_arity_of c4)) by FUNCT_6:28;
then E21: c9 in dom (the_arity_of c4) by FUNCT_1:21;
then (the_arity_of c4) . c9 in the carrier of c1 by FINSEQ_2:13;
then (the_arity_of c4) . c9 in dom the Sorts of c2 by PBOOLE:def 3;
hence c9 in dom (the Sorts of c2 * (the_arity_of c4)) by E21, FUNCT_1:21;
end;
now
let c9 be set ;
assume c9 in (c5 * (the_arity_of c4)) " (SubFuncs (rng (c5 * (the_arity_of c4)))) ;
then c9 in dom (c5 * (the_arity_of c4)) by FUNCT_6:28;
then E21: c9 in dom (the_arity_of c4) by FUNCT_1:21;
then (the_arity_of c4) . c9 in the carrier of c1 by FINSEQ_2:13;
then reconsider c10 = c5 . ((the_arity_of c4) . c9) as Function of the Sorts of c2 . ((the_arity_of c4) . c9),the Sorts of c3 . ((the_arity_of c4) . c9) by PBOOLE:def 18;
E22: ( (the Sorts of c2 * (the_arity_of c4)) . c9 = the Sorts of c2 . ((the_arity_of c4) . c9) & (the Sorts of c3 * (the_arity_of c4)) . c9 = the Sorts of c3 . ((the_arity_of c4) . c9) ) by E21, FUNCT_1:23;
(the Sorts of c3 * (the_arity_of c4)) . c9 in rng (the Sorts of c3 * (the_arity_of c4)) by E18, E19, E21, FUNCT_1:def 5;
then (the Sorts of c3 * (the_arity_of c4)) . c9 <> {} by E12, E15, CARD_3:37;
hence (the Sorts of c2 * (the_arity_of c4)) . c9 = dom c10 by E22, FUNCT_2:def 1
.= proj1 c10 by FUNCT_5:21
.= proj1 ((c5 * (the_arity_of c4)) . c9) by E21, FUNCT_1:23 ;

end;
then E21: the Sorts of c2 * (the_arity_of c4) = doms (c5 * (the_arity_of c4)) by E20, FUNCT_6:def 2;
hereby
assume c8 = c5 # c6 ;
then E22: c8 = (Frege (c5 * (the_arity_of c4))) . c6 by E12, Def7;
let c9 be Nat;
assume E23: c9 in dom c7 ;
then (the_arity_of c4) . c9 in the carrier of c1 by E16, FINSEQ_2:13;
then (the_arity_of c4) . c9 in dom c5 by PBOOLE:def 3;
then E24: c9 in dom (c5 * (the_arity_of c4)) by E16, E23, FUNCT_1:21;
then E25: (c5 * (the_arity_of c4)) . c9 = c5 . ((the_arity_of c4) . c9) by FUNCT_1:22
.= c5 . ((the_arity_of c4) /. c9) by E16, E23, FINSEQ_4:def 4 ;
thus c8 . c9 = ((c5 * (the_arity_of c4)) .. c7) . c9 by E12, E15, E21, E22, PRALG_2:def 8
.= (c5 . ((the_arity_of c4) /. c9)) . (c7 . c9) by E24, E25, PRALG_1:def 17 ;
end;
assume E22: for b1 being Nat st b1 in dom c7 holds
c8 . b1 = (c5 . ((the_arity_of c4) /. b1)) . (c7 . b1) ;
E23: rng (the_arity_of c4) c= dom c5 by E13, PBOOLE:def 3;
c5 # c6 is Element of product (the Sorts of c3 * (the_arity_of c4)) by PRALG_2:10;
then reconsider c9 = c5 # c6 as Function ;
E24: c5 # c6 = (Frege (c5 * (the_arity_of c4))) . c6 by E12, Def7;
then c5 # c6 = (c5 * (the_arity_of c4)) .. c7 by E12, E15, E21, PRALG_2:def 8;
then E25: dom c9 = dom (c5 * (the_arity_of c4)) by PRALG_1:def 17
.= dom c7 by E16, E23, RELAT_1:46 ;
now
let c10 be set ;
assume E26: c10 in dom c7 ;
then reconsider c11 = c10 as Nat by E16;
(the_arity_of c4) . c11 in the carrier of c1 by E16, E26, FINSEQ_2:13;
then (the_arity_of c4) . c11 in dom c5 by PBOOLE:def 3;
then E27: c11 in dom (c5 * (the_arity_of c4)) by E16, E26, FUNCT_1:21;
then E28: (c5 * (the_arity_of c4)) . c11 = c5 . ((the_arity_of c4) . c11) by FUNCT_1:22
.= c5 . ((the_arity_of c4) /. c11) by E16, E26, FINSEQ_4:def 4 ;
thus c8 . c10 = (c5 . ((the_arity_of c4) /. c11)) . (c7 . c11) by E22, E26
.= ((c5 * (the_arity_of c4)) .. c7) . c11 by E27, E28, PRALG_1:def 17
.= c9 . c10 by E12, E15, E21, E24, PRALG_2:def 8 ;
end;
hence c8 = c5 # c6 by E16, E19, E25, FUNCT_1:9;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be non-empty MSAlgebra of c1;
let c4 be OperSymbol of c1;
let c5 be ManySortedFunction of c2,c3;
let c6 be Element of Args c4,c2;
redefine func # as c5 # c6 -> Element of Args a4,a3 means :Def8: :: MSUALG_3:def 8
for b1 being Nat st b1 in dom a6 holds
a7 . b1 = (a5 . ((the_arity_of a4) /. b1)) . (a6 . b1);
coherence
c5 # c6 is Element of Args c4,c3 ;
compatibility
for b1 being Element of Args c4,c3 holds
( b1 = c5 # c6 iff for b2 being Nat st b2 in dom c6 holds
b1 . b2 = (c5 . ((the_arity_of c4) /. b2)) . (c6 . b2) ) by Lemma11;
end;

:: deftheorem Def8 defines # MSUALG_3:def 8 :
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being OperSymbol of b1
for b5 being ManySortedFunction of b2,b3
for b6 being Element of Args b4,b2
for b7 being Element of Args b4,b3 holds
( b7 = b5 # b6 iff for b8 being Nat st b8 in dom b6 holds
b7 . b8 = (b5 . ((the_arity_of b4) /. b8)) . (b6 . b8) );

theorem Th7: :: MSUALG_3:7
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being MSAlgebra of b1 st Args b2,b3 <> {} holds
for b4 being Element of Args b2,b3 holds b4 = (id the Sorts of b3) # b4
proof end;

theorem Th8: :: MSUALG_3:8
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3, b4, b5 being non-empty MSAlgebra of b1
for b6 being ManySortedFunction of b3,b4
for b7 being ManySortedFunction of b4,b5
for b8 being Element of Args b2,b3 holds (b7 ** b6) # b8 = b7 # (b6 # b8)
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
pred c4 is_homomorphism c2,c3 means :Def9: :: MSUALG_3:def 9
for b1 being OperSymbol of a1 st Args b1,a2 <> {} holds
for b2 being Element of Args b1,a2 holds (a4 . (the_result_sort_of b1)) . ((Den b1,a2) . b2) = (Den b1,a3) . (a4 # b2);
end;

:: deftheorem Def9 defines is_homomorphism MSUALG_3:def 9 :
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is_homomorphism b2,b3 iff for b5 being OperSymbol of b1 st Args b5,b2 <> {} holds
for b6 being Element of Args b5,b2 holds (b4 . (the_result_sort_of b5)) . ((Den b5,b2) . b6) = (Den b5,b3) . (b4 # b6) );

theorem Th9: :: MSUALG_3:9
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1 holds id the Sorts of b2 is_homomorphism b2,b2
proof end;

theorem Th10: :: MSUALG_3:10
for b1 being non empty non void ManySortedSign
for b2, b3, b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 st b5 is_homomorphism b2,b3 & b6 is_homomorphism b3,b4 holds
b6 ** b5 is_homomorphism b2,b4
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
pred c4 is_epimorphism c2,c3 means :Def10: :: MSUALG_3:def 10
( a4 is_homomorphism a2,a3 & a4 is "onto" );
end;

:: deftheorem Def10 defines is_epimorphism MSUALG_3:def 10 :
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is_epimorphism b2,b3 iff ( b4 is_homomorphism b2,b3 & b4 is "onto" ) );

theorem Th11: :: MSUALG_3:11
for b1 being non empty non void ManySortedSign
for b2, b3, b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 st b5 is_epimorphism b2,b3 & b6 is_epimorphism b3,b4 holds
b6 ** b5 is_epimorphism b2,b4
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
pred c4 is_monomorphism c2,c3 means :Def11: :: MSUALG_3:def 11
( a4 is_homomorphism a2,a3 & a4 is "1-1" );
end;

:: deftheorem Def11 defines is_monomorphism MSUALG_3:def 11 :
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is_monomorphism b2,b3 iff ( b4 is_homomorphism b2,b3 & b4 is "1-1" ) );

theorem Th12: :: MSUALG_3:12
for b1 being non empty non void ManySortedSign
for b2, b3, b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 st b5 is_monomorphism b2,b3 & b6 is_monomorphism b3,b4 holds
b6 ** b5 is_monomorphism b2,b4
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
pred c4 is_isomorphism c2,c3 means :Def12: :: MSUALG_3:def 12
( a4 is_epimorphism a2,a3 & a4 is_monomorphism a2,a3 );
end;

:: deftheorem Def12 defines is_isomorphism MSUALG_3:def 12 :
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is_isomorphism b2,b3 iff ( b4 is_epimorphism b2,b3 & b4 is_monomorphism b2,b3 ) );

theorem Th13: :: MSUALG_3:13
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is_isomorphism b2,b3 iff ( b4 is_homomorphism b2,b3 & b4 is "onto" & b4 is "1-1" ) )
proof end;

Lemma24: for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_isomorphism b2,b3 holds
b4 "" is_homomorphism b3,b2
proof end;

theorem Th14: :: MSUALG_3:14
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedFunction of b3,b2 st b4 is_isomorphism b2,b3 & b5 = b4 "" holds
b5 is_isomorphism b3,b2
proof end;

theorem Th15: :: MSUALG_3:15
for b1 being non empty non void ManySortedSign
for b2, b3, b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 st b5 is_isomorphism b2,b3 & b6 is_isomorphism b3,b4 holds
b6 ** b5 is_isomorphism b2,b4
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
pred c2,c3 are_isomorphic means :Def13: :: MSUALG_3:def 13
ex b1 being ManySortedFunction of a2,a3 st b1 is_isomorphism a2,a3;
end;

:: deftheorem Def13 defines are_isomorphic MSUALG_3:def 13 :
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1 holds
( b2,b3 are_isomorphic iff ex b4 being ManySortedFunction of b2,b3 st b4 is_isomorphism b2,b3 );

theorem Th16: :: MSUALG_3:16
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1 holds
( id the Sorts of b2 is_isomorphism b2,b2 & b2,b2 are_isomorphic )
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be MSAlgebra of c1;
redefine pred are_isomorphic as c2,c3 are_isomorphic ;
reflexivity
for b1 being MSAlgebra of c1 holds b1,b1 are_isomorphic by Th16;
end;

theorem Th17: :: MSUALG_3:17
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1 st b2,b3 are_isomorphic holds
b3,b2 are_isomorphic
proof end;

theorem Th18: :: MSUALG_3:18
for b1 being non empty non void ManySortedSign
for b2, b3, b4 being non-empty MSAlgebra of b1 st b2,b3 are_isomorphic & b3,b4 are_isomorphic holds
b2,b4 are_isomorphic
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be non-empty MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
assume E29: c4 is_homomorphism c2,c3 ;
func Image c4 -> strict non-empty MSSubAlgebra of a3 means :Def14: :: MSUALG_3:def 14
the Sorts of a5 = a4 .:.: the Sorts of a2;
existence
ex b1 being strict non-empty MSSubAlgebra of c3 st the Sorts of b1 = c4 .:.: the Sorts of c2
proof end;
uniqueness
for b1, b2 being strict non-empty MSSubAlgebra of c3 st the Sorts of b1 = c4 .:.: the Sorts of c2 & the Sorts of b2 = c4 .:.: the Sorts of c2 holds
b1 = b2 by MSUALG_2:10;
end;

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

theorem Th19: :: MSUALG_3:19
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being strict non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
( b4 is_epimorphism b2,b3 iff Image b4 = b3 )
proof end;

Lemma30: for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
b4 is ManySortedFunction of b2,(Image b4)
proof end;

theorem Th20: :: MSUALG_3:20
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedFunction of b2,(Image b4) st b4 = b5 & b4 is_homomorphism b2,b3 holds
b5 is_epimorphism b2, Image b4
proof end;

theorem Th21: :: MSUALG_3:21
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
ex b5 being ManySortedFunction of b2,(Image b4) st
( b4 = b5 & b5 is_epimorphism b2, Image b4 )
proof end;

Lemma32: for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being non-empty MSSubAlgebra of b3
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b2,b4 st b5 = b6 & b6 is_homomorphism b2,b4 holds
b5 is_homomorphism b2,b3
proof end;

theorem Th22: :: MSUALG_3:22
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being non-empty MSSubAlgebra of b2
for b4 being ManySortedFunction of b3,b2 st b4 = id the Sorts of b3 holds
b4 is_monomorphism b3,b2
proof end;

theorem Th23: :: MSUALG_3:23
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
ex b5 being ManySortedFunction of b2,(Image b4)ex b6 being ManySortedFunction of (Image b4),b3 st
( b5 is_epimorphism b2, Image b4 & b6 is_monomorphism Image b4,b3 & b4 = b6 ** b5 )
proof end;

theorem Th24: :: MSUALG_3:24
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being OperSymbol of b1
for b5 being ManySortedFunction of b2,b3
for b6 being Element of Args b4,b2
for b7, b8 being Function st b6 = b7 & b6 in Args b4,b2 & b8 in Args b4,b3 holds
( b8 = b5 # b6 iff for b9 being Nat st b9 in dom b7 holds
b8 . b9 = (b5 . ((the_arity_of b4) /. b9)) . (b7 . b9) ) by Lemma11;