let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra of S ex U0 being strict non-empty free MSAlgebra of S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
let U1 be non-empty MSAlgebra of S; :: thesis: ex U0 being strict non-empty free MSAlgebra of 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;
A1:
FreeGen the Sorts of U1 is free
by Th17;
set f = Reverse the Sorts of U1;
consider F being ManySortedFunction of (FreeMSA the Sorts of U1),U1 such that
A2:
( F is_homomorphism FreeMSA the Sorts of U1,U1 & F || (FreeGen the Sorts of U1) = Reverse the Sorts of U1 )
by A1, Def5;
reconsider fa = FreeMSA the Sorts of U1 as strict non-empty free MSAlgebra of S by Th18;
reconsider a = F as ManySortedFunction of fa,U1 ;
take
fa
; :: thesis: ex F being ManySortedFunction of fa,U1 st F is_epimorphism fa,U1
take
a
; :: thesis: a is_epimorphism fa,U1
thus
a is_homomorphism fa,U1
by A2; :: according to MSUALG_3:def 10 :: thesis: a is "onto"
thus
a is "onto"
:: thesis: verumproof
let s be
set ;
:: according to MSUALG_3:def 3 :: thesis: ( not s in the carrier of S or rng (a . s) = the Sorts of U1 . s )
assume
s in the
carrier of
S
;
:: thesis: rng (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 18;
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:99;
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= rng (a . s)
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of U1 . s or x in rng (a . s) )
assume A5:
x in the
Sorts of
U1 . s
;
:: thesis: x in rng (a . s)
set D =
DTConMSA the
Sorts of
U1;
set t =
[x,s0];
A6:
[x,s0] in Terminals (DTConMSA the Sorts of U1)
by A5, Th7;
then reconsider t =
[x,s0] as
Symbol of
(DTConMSA the Sorts of U1) ;
A7:
(Reverse the Sorts of U1) . s0 = Reverse s0,the
Sorts of
U1
by Def20;
then A8:
dom ((Reverse the Sorts of U1) . s0) = FreeGen s0,the
Sorts of
U1
by FUNCT_2:def 1;
t `2 = s0
by MCART_1:7;
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 A6;
then A9:
root-tree t in FreeGen s0,the
Sorts of
U1
by Th14;
then A10:
((Reverse the Sorts of U1) . s0) . (root-tree t) in rng ((Reverse the Sorts of U1) . s0)
by A8, FUNCT_1:def 5;
((Reverse the Sorts of U1) . s0) . (root-tree t) =
t `1
by A7, A9, Def19
.=
x
by MCART_1:7
;
hence
x in rng (a . s)
by A4, A10;
:: thesis: verum
end;