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;
A4: 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;
A5: P₁[F₂()] by A2;
A6: 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;
A7: F₃() .:.: (the carrier of F₁() --> NAT ) is V8() GeneratorSet of F₂() from BIRKHOFF:sch 5(A4, A5, A6);
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 A8: 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 A8; :: thesis: verum

end;

then doms (F₃() -hash ) = the Sorts of (FreeMSA (the carrier of F₁() --> NAT )) by MSSUBFAM:17;
then A9: (F₃() -hash ) .:.: the Sorts of (FreeMSA (the carrier of F₁() --> NAT )) = rngs (F₃() -hash ) by EQUATION:14;
A10: rngs F₃() c= rngs (F₃() -hash ) by Th1;
F₃() .:.: (the carrier of F₁() --> NAT ) c= rngs F₃() by EQUATION:13;
then A11: F₃() .:.: (the carrier of F₁() --> NAT ) c= (F₃() -hash ) .:.: Gen by A9, A10, PBOOLE:15;
F₃() -hash is_homomorphism FreeMSA (the carrier of F₁() --> NAT ),F₂() by Def1;
hence F₃() -hash is_epimorphism FreeMSA (the carrier of F₁() --> NAT ),F₂() by A7, A11, EQUATION:25; :: thesis: verum