let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for X being non-empty GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
let A be non-empty MSAlgebra over S; for X being non-empty GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
let X be non-empty GeneratorSet of A; ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
reconsider X9 = X as MSSubset of A ;
then reconsider ff = Reverse X as ManySortedFunction of FreeGen X, the Sorts of A by PBOOLE:def 15;
FreeGen X is free
by MSAFREE:16;
then consider h being ManySortedFunction of (FreeMSA X),A such that
A3:
h is_homomorphism FreeMSA X,A
and
A4:
h || (FreeGen X) = ff
;
take
h
; h is_epimorphism FreeMSA X,A
thus
h is_homomorphism FreeMSA X,A
by A3; MSUALG_3:def 8 h is "onto"
let i be set ; MSUALG_3:def 3 ( not i in the carrier of S or proj2 (h . i) = the Sorts of A . i )
assume
i in the carrier of S
; proj2 (h . i) = the Sorts of A . i
then reconsider s = i as SortSymbol of S ;
set f = h . s;
consider g being ManySortedFunction of (FreeMSA X),(Image h) such that
A5:
h = g
and
A6:
g is_epimorphism FreeMSA X, Image h
by A3, MSUALG_3:21;
A7:
g is_homomorphism FreeMSA X, Image h
by A6;
A8:
Image g = Image h
by A6, MSUALG_3:19;
X is MSSubset of (Image h)
proof
let i be
object ;
PBOOLE:def 2,
PBOOLE:def 18 ( not i in the carrier of S or X . i c= the Sorts of (Image h) . i )
assume A9:
i in the
carrier of
S
;
X . i c= the Sorts of (Image h) . i
then reconsider s =
i as
SortSymbol of
S ;
s in dom (Reverse X)
by A9, PARTFUN1:def 2;
then A10:
(
rngs (Reverse X) = X &
(rngs (Reverse X)) . s = rng ((Reverse X) . s) )
by EXTENS_1:10, FUNCT_6:22;
reconsider hs =
h . s as
Function of
( the Sorts of (FreeMSA X) . s),
( the Sorts of A . s) ;
let x be
object ;
TARSKI:def 3 ( not x in X . i or x in the Sorts of (Image h) . i )
FreeGen X c= the
Sorts of
(FreeMSA X)
by PBOOLE:def 18;
then A11:
(FreeGen X) . s c= the
Sorts of
(FreeMSA X) . s
;
the
Sorts of
(Image h) = h .:.: the
Sorts of
(FreeMSA X)
by A3, MSUALG_3:def 12;
then A12:
the
Sorts of
(Image h) . s = hs .: ( the Sorts of (FreeMSA X) . s)
by PBOOLE:def 20;
assume
x in X . i
;
x in the Sorts of (Image h) . i
then consider c being
object such that A13:
c in dom (ff . s)
and A14:
x = (ff . s) . c
by A10, FUNCT_1:def 3;
A15:
ff . s = hs | ((FreeGen X) . s)
by A4, MSAFREE:def 1;
then
dom (ff . s) = (dom hs) /\ ((FreeGen X) . s)
by RELAT_1:61;
then A16:
(
c in (FreeGen X) . s &
c in dom hs )
by A13, XBOOLE_0:def 4;
x = hs . c
by A15, A13, A14, FUNCT_1:47;
hence
x in the
Sorts of
(Image h) . i
by A12, A11, A16, FUNCT_1:def 6;
verum
end;
then
GenMSAlg X9 is MSSubAlgebra of Image h
by MSUALG_2:def 17;
then
the Sorts of (GenMSAlg X9) is MSSubset of (Image h)
by MSUALG_2:def 9;
then A17:
the Sorts of (GenMSAlg X9) c= the Sorts of (Image h)
by PBOOLE:def 18;
the Sorts of (Image g) = h .:.: the Sorts of (FreeMSA X)
by A5, A7, MSUALG_3:def 12;
then A18:
the Sorts of (Image g) . i = (h . s) .: ( the Sorts of (FreeMSA X) . i)
by PBOOLE:def 20;
the Sorts of (Image h) is MSSubset of A
by MSUALG_2:def 9;
then
( the Sorts of (GenMSAlg X9) = the Sorts of A & the Sorts of (Image h) c= the Sorts of A )
by MSAFREE:def 4, PBOOLE:def 18;
then
the Sorts of (Image h) = the Sorts of A
by A17, PBOOLE:146;
hence
proj2 (h . i) = the Sorts of A . i
by A18, A8, RELSET_1:22; verum