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 () as MSSubset of () by PBOOLE:def 18;
A11: GEN is GeneratorSet of F2() by ;
reconsider sI = the Sorts of () as MSSubset of F2() by MSUALG_2:def 9;
GEN is ManySortedSubset of sI
proof
let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in the carrier of F1() or GEN . i c= sI . i )
assume i in the carrier of F1() ; :: thesis: GEN . i c= sI . i
then reconsider s = i as SortSymbol of F1() ;
let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in GEN . i or g in sI . i )
assume A12: g in GEN . i ; :: thesis: 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 ;
then consider x being object such that
A15: x in dom (F . s) and
A16: g = (F . s) . x by ;
dom (F . s) = NAT by FUNCT_2:def 1
.= dom fi by FUNCT_2:def 1 ;
then A17: fi . x in rng fi by ;
g = ((h . s) * fi) . x by
.= (h . s) . (fi . x) by ;
then g in (h . s) .: ( the Sorts of F3() . s) by ;
then g in (h .:.: the Sorts of F3()) . s by PBOOLE:def 20;
hence g in sI . i by ; :: thesis: 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 ;
then F2() is MSSubAlgebra of Image h by ;
then F2() = Image h by MSUALG_2:7;
then A19: h is_epimorphism F3(),F2() by ;
P1[ QuotMSAlg (F3(),())] by A2, A5;
hence P1[F2()] by A4, A19, MSUALG_4:6; :: thesis: verum