set I = the carrier of F₁();
set sA = the Sorts of F₂();
consider Gen being GeneratorSet of F₂() such that
A6: Gen is finite-yielding by MSAFREE2:def 10;
reconsider Gen = Gen as finite-yielding ManySortedSubset of the Sorts of F₂() by A6;
consider GEN being non-empty finite-yielding ManySortedSubset of the Sorts of F₂() such that
A7: Gen c= GEN by MSUALG_9:7;
consider F being ManySortedFunction of the carrier of F₁() --> NAT,GEN such that
A8: F is "onto" by MSUALG_9:12;
the carrier of F₁() --> NAT is_transformable_to GEN ;
then reconsider G = F as ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂() by EXTENS_1:5;
consider h being ManySortedFunction of F₃(),F₂() such that
A9: h is_homomorphism F₃(),F₂() and
A10: G = h ** F₄() 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₂() by A7, MSSCYC_1:21;
reconsider sI = the Sorts of (Image h) as MSSubset of F₂() 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 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₁() ;
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₄() . s as sequence of ( the Sorts of F₃() . 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₃() . s) by A17, A14, FUNCT_1:def 6;
then g in (h .:.: the Sorts of F₃()) . s by PBOOLE:def 20;
hence g in sI . i by A9, MSUALG_3:def 12; :: 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 A18, MSUALG_2:21;
then F₂() is MSSubAlgebra of Image h by A11, MSAFREE:3;
then F₂() = Image h by MSUALG_2:7;
then A19: h is_epimorphism F₃(),F₂() by A9, MSUALG_3:19;
P₁[ QuotMSAlg (F₃(),(MSCng h))] by A2, A5;
hence P₁[F₂()] by A4, A19, MSUALG_4:6; :: thesis: verum