let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1

let U1 be non-empty MSAlgebra over S; :: thesis: ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1

set S1 = the Sorts of U1;

set FA = FreeMSA the Sorts of U1;

set FG = FreeGen the Sorts of U1;

reconsider fa = FreeMSA the Sorts of U1 as strict non-empty free MSAlgebra over S by Th17;

set f = Reverse the Sorts of U1;

take fa ; :: thesis: ex F being ManySortedFunction of fa,U1 st F is_epimorphism fa,U1

FreeGen the Sorts of U1 is free by Th16;

then consider F being ManySortedFunction of (FreeMSA the Sorts of U1),U1 such that

A1: F is_homomorphism FreeMSA the Sorts of U1,U1 and

A2: F || (FreeGen the Sorts of U1) = Reverse the Sorts of U1 ;

reconsider a = F as ManySortedFunction of fa,U1 ;

take a ; :: thesis: a is_epimorphism fa,U1

thus a is_homomorphism fa,U1 by A1; :: according to MSUALG_3:def 8 :: thesis: a is "onto"

thus a is "onto" :: thesis: verum

let U1 be non-empty MSAlgebra over S; :: thesis: ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1

set S1 = the Sorts of U1;

set FA = FreeMSA the Sorts of U1;

set FG = FreeGen the Sorts of U1;

reconsider fa = FreeMSA the Sorts of U1 as strict non-empty free MSAlgebra over S by Th17;

set f = Reverse the Sorts of U1;

take fa ; :: thesis: ex F being ManySortedFunction of fa,U1 st F is_epimorphism fa,U1

FreeGen the Sorts of U1 is free by Th16;

then consider F being ManySortedFunction of (FreeMSA the Sorts of U1),U1 such that

A1: F is_homomorphism FreeMSA the Sorts of U1,U1 and

A2: F || (FreeGen the Sorts of U1) = Reverse the Sorts of U1 ;

reconsider a = F as ManySortedFunction of fa,U1 ;

take a ; :: thesis: a is_epimorphism fa,U1

thus a is_homomorphism fa,U1 by A1; :: according to MSUALG_3:def 8 :: thesis: a is "onto"

thus a is "onto" :: thesis: verum

proof

let s be set ; :: according to MSUALG_3:def 3 :: thesis: ( not s in the carrier of S or proj2 (a . s) = the Sorts of U1 . s )

assume s in the carrier of S ; :: thesis: proj2 (a . s) = the Sorts of U1 . s

then reconsider s0 = s as SortSymbol of S ;

reconsider g = a . s as Function of ( the Sorts of fa . s0),( the Sorts of U1 . s0) by PBOOLE:def 15;

A3: (Reverse the Sorts of U1) . s0 = g | ((FreeGen the Sorts of U1) . s0) by A2, Def1;

then A4: rng ((Reverse the Sorts of U1) . s0) c= rng g by RELAT_1:70;

thus rng (a . s) c= the Sorts of U1 . s by A3, RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of U1 . s c= proj2 (a . s)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of U1 . s or x in proj2 (a . s) )

set D = DTConMSA the Sorts of U1;

set t = [x,s0];

assume x in the Sorts of U1 . s ; :: thesis: x in proj2 (a . s)

then A5: [x,s0] in Terminals (DTConMSA the Sorts of U1) by Th7;

then reconsider t = [x,s0] as Symbol of (DTConMSA the Sorts of U1) ;

t `2 = s0 ;

then root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA the Sorts of U1) : ( tt in Terminals (DTConMSA the Sorts of U1) & tt `2 = s0 ) } by A5;

then A6: root-tree t in FreeGen (s0, the Sorts of U1) by Th13;

A7: (Reverse the Sorts of U1) . s0 = Reverse (s0, the Sorts of U1) by Def18;

then dom ((Reverse the Sorts of U1) . s0) = FreeGen (s0, the Sorts of U1) by FUNCT_2:def 1;

then A8: ((Reverse the Sorts of U1) . s0) . (root-tree t) in rng ((Reverse the Sorts of U1) . s0) by A6, FUNCT_1:def 3;

((Reverse the Sorts of U1) . s0) . (root-tree t) = t `1 by A7, A6, Def17

.= x ;

hence x in proj2 (a . s) by A4, A8; :: thesis: verum

end;assume s in the carrier of S ; :: thesis: proj2 (a . s) = the Sorts of U1 . s

then reconsider s0 = s as SortSymbol of S ;

reconsider g = a . s as Function of ( the Sorts of fa . s0),( the Sorts of U1 . s0) by PBOOLE:def 15;

A3: (Reverse the Sorts of U1) . s0 = g | ((FreeGen the Sorts of U1) . s0) by A2, Def1;

then A4: rng ((Reverse the Sorts of U1) . s0) c= rng g by RELAT_1:70;

thus rng (a . s) c= the Sorts of U1 . s by A3, RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of U1 . s c= proj2 (a . s)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of U1 . s or x in proj2 (a . s) )

set D = DTConMSA the Sorts of U1;

set t = [x,s0];

assume x in the Sorts of U1 . s ; :: thesis: x in proj2 (a . s)

then A5: [x,s0] in Terminals (DTConMSA the Sorts of U1) by Th7;

then reconsider t = [x,s0] as Symbol of (DTConMSA the Sorts of U1) ;

t `2 = s0 ;

then root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA the Sorts of U1) : ( tt in Terminals (DTConMSA the Sorts of U1) & tt `2 = s0 ) } by A5;

then A6: root-tree t in FreeGen (s0, the Sorts of U1) by Th13;

A7: (Reverse the Sorts of U1) . s0 = Reverse (s0, the Sorts of U1) by Def18;

then dom ((Reverse the Sorts of U1) . s0) = FreeGen (s0, the Sorts of U1) by FUNCT_2:def 1;

then A8: ((Reverse the Sorts of U1) . s0) . (root-tree t) in rng ((Reverse the Sorts of U1) . s0) by A6, FUNCT_1:def 3;

((Reverse the Sorts of U1) . s0) . (root-tree t) = t `1 by A7, A6, Def17

.= x ;

hence x in proj2 (a . s) by A4, A8; :: thesis: verum