A4: P1[F2()] by A2;
set V = the carrier of F1() --> NAT;
reconsider Gen = the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) as GeneratorSet of FreeMSA ( the carrier of F1() --> NAT) by MSAFREE2:6;
A5: F3() .:.: ( the carrier of F1() --> NAT) c= rngs F3() by EQUATION:12;
the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) is_transformable_to the Sorts of F2() ;
then doms (F3() -hash) = the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) by MSSUBFAM:17;
then A6: (F3() -hash) .:.: the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) = rngs (F3() -hash) by EQUATION:13;
rngs F3() c= rngs (F3() -hash) by Th1;
then A7: F3() .:.: ( the carrier of F1() --> NAT) c= (F3() -hash) .:.: Gen by ;
A8: F3() -hash is_homomorphism FreeMSA ( the carrier of F1() --> NAT),F2() by Def1;
A9: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] by A3;
A10: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex H being ManySortedFunction of F2(),C st
( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
H = K ) ) by A1;
F3() .:.: ( the carrier of F1() --> NAT) is V2() GeneratorSet of F2() from hence F3() -hash is_epimorphism FreeMSA ( the carrier of F1() --> NAT),F2() by ; :: thesis: verum