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:6;
A5: F₃() .:.: ( the carrier of F₁() --> NAT) c= rngs F₃() by EQUATION:12;
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:13;
rngs F₃() c= rngs (F₃() -hash) by Th1;
then A8: F₃() .:.: ( the carrier of F₁() --> NAT) c= (F₃() -hash) .:.: Gen by A7, A5, PBOOLE:13;
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:23; :: thesis: verum