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