set I = the carrier of F₁();
set sA = the Sorts of F₂();
consider Gen being GeneratorSet of F₂() such that
A6: Gen is locally-finite by MSAFREE2:def 10;
reconsider Gen = Gen as V27 ManySortedSubset of the Sorts of F₂() by A6;
consider GEN being V8 V27 ManySortedSubset of the Sorts of F₂() such that
A7: Gen c= GEN by MSUALG_9:8;
consider F being ManySortedFunction of the carrier of F₁() --> NAT ,GEN such that
A8: F is "onto" by MSUALG_9:13;
the carrier of F₁() --> NAT is_transformable_to GEN

proof

let i be set ; :: according to PZFMISC1:def 3 :: thesis: ( not i in the carrier of F₁() or not GEN . i = {} or (the carrier of F₁() --> NAT ) . i = {} )
assume i in the carrier of F₁() ; :: thesis: ( not GEN . i = {} or (the carrier of F₁() --> NAT ) . i = {} )
hence ( not GEN . i = {} or (the carrier of F₁() --> NAT ) . i = {} ) ; :: thesis: verum

end;

then reconsider G = F as ManySortedFunction of the carrier of F₁() --> NAT ,the Sorts of F₂() by EXTENS_1:9;
consider h being ManySortedFunction of F₃(),F₂() such that
A9: h is_homomorphism F₃(),F₂() and
A10: G = h ** F₄() by A1, A3;
A11: P₁[ QuotMSAlg F₃(),(MSCng h)] by A2, A5;
reconsider sI = the Sorts of (Image h) as MSSubset of F₂() by MSUALG_2:def 10;
the Sorts of (Image h) is ManySortedSubset of the Sorts of (Image h)

proof

thus the Sorts of (Image h) c= the Sorts of (Image h) ; :: according to PBOOLE:def 23 :: thesis: verum

end;

then reconsider sI1 = the Sorts of (Image h) as MSSubset of (Image h) ;
GEN is ManySortedSubset of sI

proof

let i be set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: thesis: ( not i in the carrier of F₁() or GEN . i c= sI . i )
assume i in the carrier of F₁() ; :: thesis: GEN . i c= sI . i
then reconsider s = i as SortSymbol of F₁() ;
A12: rng (F . s) = GEN . s by A8, MSUALG_3:def 3;
A13: (the carrier of F₁() --> NAT ) . s = NAT by FUNCOP_1:13;
then reconsider fi = F₄() . s as Function of NAT ,the Sorts of F₃() . s ;
let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in GEN . i or g in sI . i )
assume g in GEN . i ; :: thesis: g in sI . i
then consider x being set such that
A14: x in dom (F . s) and
A15: g = (F . s) . x by A12, FUNCT_1:def 5;
dom (F . s) = NAT by A13, FUNCT_2:def 1
.= dom fi by FUNCT_2:def 1 ;
then A16: fi . x in rng fi by A14, FUNCT_1:def 5;
dom ((h . s) * fi) = NAT by FUNCT_2:def 1
.= dom fi by FUNCT_2:def 1 ;
then A17: rng fi c= dom (h . s) by FUNCT_1:27;
g = ((h . s) * fi) . x by A10, A15, MSUALG_3:2
.= (h . s) . (fi . x) by A14, FUNCT_2:21 ;
then g in (h . s) .: (the Sorts of F₃() . s) by A16, A17, FUNCT_1:def 12;
then g in (h .:.: the Sorts of F₃()) . s by PBOOLE:def 25;
hence g in sI . i by A9, MSUALG_3:def 14; :: thesis: verum

end;

then A18: GenMSAlg GEN is MSSubAlgebra of GenMSAlg sI by EXTENS_1:21;
GenMSAlg sI = GenMSAlg sI1 by EXTENS_1:22;
then A19: GenMSAlg GEN is MSSubAlgebra of Image h by A18, MSUALG_2:22;
GEN is GeneratorSet of F₂() by A7, MSSCYC_1:21;
then F₂() is MSSubAlgebra of Image h by A19, MSAFREE:3;
then F₂() = Image h by MSUALG_2:8;
then h is_epimorphism F₃(),F₂() by A9, MSUALG_3:19;
hence P₁[F₂()] by A4, A11, MSUALG_4:6; :: thesis: verum