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₂() ;
then doms (F₃() -hash) = the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) by MSSUBFAM:17;
then A6: (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 A7: F₃() .:.: ( the carrier of F₁() --> NAT) c= (F₃() -hash) .:.: Gen by A6, A5, PBOOLE:13;
A8: F₃() -hash is_homomorphism FreeMSA ( the carrier of F₁() --> NAT),F₂() by Def1;
A9: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] by A3;
A10: for C being non-empty MSAlgebra over 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 non-empty GeneratorSet of F₂() from BIRKHOFF:sch 5(A10, A4, A9);
hence F₃() -hash is_epimorphism FreeMSA ( the carrier of F₁() --> NAT),F₂() by A7, A8, EQUATION:23; :: thesis: verum