A4: P₁[F₂()] by A2;
set V = the carrier of F₁() --> NAT ;
reconsider Gen = the Sorts of (FreeMSA (the carrier of F₁() --> NAT )) as GeneratorSet of FreeMSA (the carrier of F₁() --> NAT ) by MSAFREE2:9;
A5: F₃() .:.: (the carrier of F₁() --> NAT ) c= rngs F₃() by EQUATION:13;
the Sorts of (FreeMSA (the carrier of F₁() --> NAT )) is_transformable_to the Sorts of F₂()

proof

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

end;

then doms (F₃() -hash ) = the Sorts of (FreeMSA (the carrier of F₁() --> NAT )) by MSSUBFAM:17;
then A7: (F₃() -hash ) .:.: the Sorts of (FreeMSA (the carrier of F₁() --> NAT )) = rngs (F₃() -hash ) by EQUATION:14;
rngs F₃() c= rngs (F₃() -hash ) by Th1;
then A8: F₃() .:.: (the carrier of F₁() --> NAT ) c= (F₃() -hash ) .:.: Gen by A7, A5, PBOOLE:15;
A9: F₃() -hash is_homomorphism FreeMSA (the carrier of F₁() --> NAT ),F₂() by Def1;
A10: for A being non-empty MSAlgebra of F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] by A3;
A11: for C being non-empty MSAlgebra of F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT ,the Sorts of C st P₁[C] holds
ex H being ManySortedFunction of F₂(),C st
( H is_homomorphism F₂(),C & H ** F₃() = G & ( for K being ManySortedFunction of F₂(),C st K is_homomorphism F₂(),C & K ** F₃() = G holds
H = K ) ) by A1;
F₃() .:.: (the carrier of F₁() --> NAT ) is V8() GeneratorSet of F₂() from BIRKHOFF:sch 5(A11, A4, A10);
hence F₃() -hash is_epimorphism FreeMSA (the carrier of F₁() --> NAT ),F₂() by A8, A9, EQUATION:25; :: thesis: verum