let S be non empty non void ManySortedSign ; 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; 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
; 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
; a is_epimorphism fa,U1
thus
a is_homomorphism fa,U1
by A1; MSUALG_3:def 8 a is "onto"
thus
a is "onto"
verumproof
let s be
set ;
MSUALG_3:def 3 ( not s in the carrier of S or proj2 (a . s) = the Sorts of U1 . s )
assume
s in the
carrier of
S
;
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;
XBOOLE_0:def 10 the Sorts of U1 . s c= proj2 (a . s)
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;