let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
let A be non-empty MSAlgebra of S; :: thesis: for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
let X be V2() GeneratorSet of A; :: thesis: ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
then reconsider ff = Reverse X as ManySortedFunction of FreeGen X,the Sorts of A by PBOOLE:def 18;
FreeGen X is free
by MSAFREE:17;
then consider h being ManySortedFunction of (FreeMSA X),A such that
A4:
( h is_homomorphism FreeMSA X,A & h || (FreeGen X) = ff )
by MSAFREE:def 5;
take
h
; :: thesis: h is_epimorphism FreeMSA X,A
thus
h is_homomorphism FreeMSA X,A
by A4; :: according to MSUALG_3:def 10 :: thesis: h is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in the carrier of S or rng (h . i) = the Sorts of A . i )
consider g being ManySortedFunction of (FreeMSA X),(Image h) such that
A5:
( h = g & g is_epimorphism FreeMSA X, Image h )
by A4, MSUALG_3:21;
reconsider X' = X as MSSubset of A ;
X is MSSubset of (Image h)
proof
let i be
set ;
:: according to PBOOLE:def 5,
PBOOLE:def 23 :: thesis: ( not i in the carrier of S or X . i c= the Sorts of (Image h) . i )
assume A6:
i in the
carrier of
S
;
:: thesis: X . i c= the Sorts of (Image h) . i
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in X . i or x in the Sorts of (Image h) . i )
assume A7:
x in X . i
;
:: thesis: x in the Sorts of (Image h) . i
reconsider s =
i as
SortSymbol of
S by A6;
reconsider hs =
h . s as
Function of
(the Sorts of (FreeMSA X) . s),
(the Sorts of A . s) ;
the
Sorts of
(Image h) = h .:.: the
Sorts of
(FreeMSA X)
by A4, MSUALG_3:def 14;
then A8:
the
Sorts of
(Image h) . s = hs .: (the Sorts of (FreeMSA X) . s)
by PBOOLE:def 25;
A9:
ff . s = hs | ((FreeGen X) . s)
by A4, MSAFREE:def 1;
A10:
rngs (Reverse X) = X
by EXTENS_1:14;
s in dom (Reverse X)
by A6, PARTFUN1:def 4;
then
(rngs (Reverse X)) . s = rng ((Reverse X) . s)
by FUNCT_6:31;
then consider c being
set such that A11:
(
c in dom (ff . s) &
x = (ff . s) . c )
by A7, A10, FUNCT_1:def 5;
(
dom (ff . s) = (dom hs) /\ ((FreeGen X) . s) &
(ff . s) . c = hs . c )
by A9, A11, FUNCT_1:70, RELAT_1:90;
then A12:
(
c in dom hs &
c in (FreeGen X) . s )
by A11, XBOOLE_0:def 4;
FreeGen X c= the
Sorts of
(FreeMSA X)
by PBOOLE:def 23;
then
(FreeGen X) . s c= the
Sorts of
(FreeMSA X) . s
by PBOOLE:def 5;
then
(
c in dom hs &
c in the
Sorts of
(FreeMSA X) . s &
x = hs . c )
by A9, A11, A12, FUNCT_1:70;
hence
x in the
Sorts of
(Image h) . i
by A8, FUNCT_1:def 12;
:: thesis: verum
end;
then
GenMSAlg X' is MSSubAlgebra of Image h
by MSUALG_2:def 18;
then
the Sorts of (GenMSAlg X') is MSSubset of (Image h)
by MSUALG_2:def 10;
then A13:
the Sorts of (GenMSAlg X') c= the Sorts of (Image h)
by PBOOLE:def 23;
A14:
the Sorts of (GenMSAlg X') = the Sorts of A
by MSAFREE:def 4;
the Sorts of (Image h) is MSSubset of A
by MSUALG_2:def 10;
then
the Sorts of (Image h) c= the Sorts of A
by PBOOLE:def 23;
then A15:
the Sorts of (Image h) = the Sorts of A
by A13, A14, PBOOLE:def 13;
assume
i in the carrier of S
; :: thesis: rng (h . i) = the Sorts of A . i
then reconsider s = i as SortSymbol of S ;
set f = h . s;
A16:
g is_homomorphism FreeMSA X, Image h
by A5, MSUALG_3:def 10;
then
the Sorts of (Image g) = h .:.: the Sorts of (FreeMSA X)
by A5, MSUALG_3:def 14;
then A17:
the Sorts of (Image g) . i = (h . s) .: (the Sorts of (FreeMSA X) . i)
by PBOOLE:def 25;
Image g = Image h
by A5, A16, MSUALG_3:19;
hence
rng (h . i) = the Sorts of A . i
by A15, A17, FUNCT_2:45; :: thesis: verum