set I = the carrier of F1();
set sA = the Sorts of F2();
consider Gen being GeneratorSet of F2() such that
A6:
Gen is V45()
by MSAFREE2:def 10;
reconsider Gen = Gen as V45() ManySortedSubset of the Sorts of F2() by A6;
consider GEN being V2() V45() ManySortedSubset of the Sorts of F2() such that
A7:
Gen c= GEN
by MSUALG_9:7;
consider F being ManySortedFunction of the carrier of F1() --> NAT,GEN such that
A8:
F is "onto"
by MSUALG_9:12;
the carrier of F1() --> NAT is_transformable_to GEN
;
then reconsider G = F as ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2() by EXTENS_1:5;
consider h being ManySortedFunction of F3(),F2() such that
A9:
h is_homomorphism F3(),F2()
and
A10:
G = h ** F4()
by A1, A3;
reconsider sI1 = the Sorts of (Image h) as MSSubset of (Image h) by PBOOLE:def 18;
A11:
GEN is GeneratorSet of F2()
by A7, MSSCYC_1:21;
reconsider sI = the Sorts of (Image h) as MSSubset of F2() by MSUALG_2:def 9;
GEN is ManySortedSubset of sI
proof
let i be
object ;
PBOOLE:def 2,
PBOOLE:def 18 ( not i in the carrier of F1() or GEN . i c= sI . i )
assume
i in the
carrier of
F1()
;
GEN . i c= sI . i
then reconsider s =
i as
SortSymbol of
F1() ;
let g be
object ;
TARSKI:def 3 ( not g in GEN . i or g in sI . i )
assume A12:
g in GEN . i
;
g in sI . i
reconsider fi =
F4()
. s as
sequence of
( the Sorts of F3() . s) ;
dom ((h . s) * fi) =
NAT
by FUNCT_2:def 1
.=
dom fi
by FUNCT_2:def 1
;
then A14:
rng fi c= dom (h . s)
by FUNCT_1:15;
rng (F . s) = GEN . s
by A8, MSUALG_3:def 3;
then consider x being
object such that A15:
x in dom (F . s)
and A16:
g = (F . s) . x
by A12, FUNCT_1:def 3;
dom (F . s) =
NAT
by FUNCT_2:def 1
.=
dom fi
by FUNCT_2:def 1
;
then A17:
fi . x in rng fi
by A15, FUNCT_1:def 3;
g =
((h . s) * fi) . x
by A10, A16, MSUALG_3:2
.=
(h . s) . (fi . x)
by A15, FUNCT_2:15
;
then
g in (h . s) .: ( the Sorts of F3() . s)
by A17, A14, FUNCT_1:def 6;
then
g in (h .:.: the Sorts of F3()) . s
by PBOOLE:def 20;
hence
g in sI . i
by A9, MSUALG_3:def 12;
verum
end;
then A18:
GenMSAlg GEN is MSSubAlgebra of GenMSAlg sI
by EXTENS_1:17;
GenMSAlg sI = GenMSAlg sI1
by EXTENS_1:18;
then
GenMSAlg GEN is MSSubAlgebra of Image h
by A18, MSUALG_2:21;
then
F2() is MSSubAlgebra of Image h
by A11, MSAFREE:3;
then
F2() = Image h
by MSUALG_2:7;
then A19:
h is_epimorphism F3(),F2()
by A9, MSUALG_3:19;
P1[ QuotMSAlg (F3(),(MSCng h))]
by A2, A5;
hence
P1[F2()]
by A4, A19, MSUALG_4:6; verum