set I = the carrier of F_{1}();

set sA = the Sorts of F_{2}();

consider Gen being GeneratorSet of F_{2}() such that

A6: Gen is V45() by MSAFREE2:def 10;

reconsider Gen = Gen as V45() ManySortedSubset of the Sorts of F_{2}() by A6;

consider GEN being V2() V45() ManySortedSubset of the Sorts of F_{2}() such that

A7: Gen c= GEN by MSUALG_9:7;

consider F being ManySortedFunction of the carrier of F_{1}() --> NAT,GEN such that

A8: F is "onto" by MSUALG_9:12;

the carrier of F_{1}() --> NAT is_transformable_to GEN
;

then reconsider G = F as ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{2}() by EXTENS_1:5;

consider h being ManySortedFunction of F_{3}(),F_{2}() such that

A9: h is_homomorphism F_{3}(),F_{2}()
and

A10: G = h ** F_{4}()
by A1, A3;

reconsider sI1 = the Sorts of (Image h) as MSSubset of (Image h) by PBOOLE:def 18;

A11: GEN is GeneratorSet of F_{2}()
by A7, MSSCYC_1:21;

reconsider sI = the Sorts of (Image h) as MSSubset of F_{2}() by MSUALG_2:def 9;

GEN is ManySortedSubset of sI

GenMSAlg sI = GenMSAlg sI1 by EXTENS_1:18;

then GenMSAlg GEN is MSSubAlgebra of Image h by A18, MSUALG_2:21;

then F_{2}() is MSSubAlgebra of Image h
by A11, MSAFREE:3;

then F_{2}() = Image h
by MSUALG_2:7;

then A19: h is_epimorphism F_{3}(),F_{2}()
by A9, MSUALG_3:19;

P_{1}[ QuotMSAlg (F_{3}(),(MSCng h))]
by A2, A5;

hence P_{1}[F_{2}()]
by A4, A19, MSUALG_4:6; :: thesis: verum

set sA = the Sorts of F

consider Gen being GeneratorSet of F

A6: Gen is V45() by MSAFREE2:def 10;

reconsider Gen = Gen as V45() ManySortedSubset of the Sorts of F

consider GEN being V2() V45() ManySortedSubset of the Sorts of F

A7: Gen c= GEN by MSUALG_9:7;

consider F being ManySortedFunction of the carrier of F

A8: F is "onto" by MSUALG_9:12;

the carrier of F

then reconsider G = F as ManySortedFunction of the carrier of F

consider h being ManySortedFunction of F

A9: h is_homomorphism F

A10: G = h ** F

reconsider sI1 = the Sorts of (Image h) as MSSubset of (Image h) by PBOOLE:def 18;

A11: GEN is GeneratorSet of F

reconsider sI = the Sorts of (Image h) as MSSubset of F

GEN is ManySortedSubset of sI

proof

then A18:
GenMSAlg GEN is MSSubAlgebra of GenMSAlg sI
by EXTENS_1:17;
let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in the carrier of F_{1}() or GEN . i c= sI . i )

assume i in the carrier of F_{1}()
; :: thesis: GEN . i c= sI . i

then reconsider s = i as SortSymbol of F_{1}() ;

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 = F_{4}() . s as sequence of ( the Sorts of F_{3}() . 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 F_{3}() . s)
by A17, A14, FUNCT_1:def 6;

then g in (h .:.: the Sorts of F_{3}()) . s
by PBOOLE:def 20;

hence g in sI . i by A9, MSUALG_3:def 12; :: thesis: verum

end;assume i in the carrier of F

then reconsider s = i as SortSymbol of F

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 = F

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 F

then g in (h .:.: the Sorts of F

hence g in sI . i by A9, MSUALG_3:def 12; :: thesis: verum

GenMSAlg sI = GenMSAlg sI1 by EXTENS_1:18;

then GenMSAlg GEN is MSSubAlgebra of Image h by A18, MSUALG_2:21;

then F

then F

then A19: h is_epimorphism F

P

hence P