A4:
P_{1}[F_{2}()]
by A2;

set V = the carrier of F_{1}() --> NAT;

reconsider Gen = the Sorts of (FreeMSA ( the carrier of F_{1}() --> NAT)) as GeneratorSet of FreeMSA ( the carrier of F_{1}() --> NAT) by MSAFREE2:6;

A5: F_{3}() .:.: ( the carrier of F_{1}() --> NAT) c= rngs F_{3}()
by EQUATION:12;

the Sorts of (FreeMSA ( the carrier of F_{1}() --> NAT)) is_transformable_to the Sorts of F_{2}()
;

then doms (F_{3}() -hash) = the Sorts of (FreeMSA ( the carrier of F_{1}() --> NAT))
by MSSUBFAM:17;

then A6: (F_{3}() -hash) .:.: the Sorts of (FreeMSA ( the carrier of F_{1}() --> NAT)) = rngs (F_{3}() -hash)
by EQUATION:13;

rngs F_{3}() c= rngs (F_{3}() -hash)
by Th1;

then A7: F_{3}() .:.: ( the carrier of F_{1}() --> NAT) c= (F_{3}() -hash) .:.: Gen
by A6, A5, PBOOLE:13;

A8: F_{3}() -hash is_homomorphism FreeMSA ( the carrier of F_{1}() --> NAT),F_{2}()
by Def1;

A9: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
by A3;

A10: for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{1}[C] holds

ex H being ManySortedFunction of F_{2}(),C st

( H is_homomorphism F_{2}(),C & H ** F_{3}() = G & ( for K being ManySortedFunction of F_{2}(),C st K is_homomorphism F_{2}(),C & K ** F_{3}() = G holds

H = K ) ) by A1;

F_{3}() .:.: ( the carrier of F_{1}() --> NAT) is V2() GeneratorSet of F_{2}()
from BIRKHOFF:sch 5(A10, A4, A9);

hence F_{3}() -hash is_epimorphism FreeMSA ( the carrier of F_{1}() --> NAT),F_{2}()
by A7, A8, EQUATION:23; :: thesis: verum

set V = the carrier of F

reconsider Gen = the Sorts of (FreeMSA ( the carrier of F

A5: F

the Sorts of (FreeMSA ( the carrier of F

then doms (F

then A6: (F

rngs F

then A7: F

A8: F

A9: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

A10: for C being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of F

( H is_homomorphism F

H = K ) ) by A1;

F

hence F