set V = the carrier of F1() --> NAT ;
A7: for A being non-empty MSAlgebra of F1() holds
( P2[A] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra of F1() st P1[B] holds
B |= e ) holds
A |= e ) by A1;
A8: for A, B being non-empty MSAlgebra of F1() st A,B are_isomorphic & P1[A] holds
P1[B] by A4;
A9: for A being non-empty MSAlgebra of F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] by A5;
A10: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra of F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F] by A6;
consider A being strict non-empty MSAlgebra of F1(), fi being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of A such that
A11: P1[A] and
A12: for B being non-empty MSAlgebra of F1()
for G being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of B st P1[B] holds
ex H being ManySortedFunction of A,B st
( H is_homomorphism A,B & H ** fi = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** fi = G holds
H = K ) ) from BIRKHOFF:sch 2(A8, A9, A10);
 A13: P2[A] from BIRKHOFF:sch 10(A7, A11);
 A14: F3() -hash is_homomorphism FreeMSA (the carrier of F1() --> NAT ),F2() by Def1;
A15: for C being non-empty MSAlgebra of F1()
for G being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C st P2[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F3() )
proof
let C be non-empty MSAlgebra of F1(); :: thesis: for G being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C st P2[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F3() )
let G be ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C; :: thesis: ( P2[C] implies ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F3() ) )
assume P2[C] ; :: thesis: ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F3() )
then consider h being ManySortedFunction of F2(),C such that
A16: ( h is_homomorphism F2(),C & G = h ** F3() ) and
for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
h = K by A2;
take h ; :: thesis: ( h is_homomorphism F2(),C & G = h ** F3() )
thus ( h is_homomorphism F2(),C & G = h ** F3() ) by A16; :: thesis: verum
end;
A17: for C being non-empty MSAlgebra of F1()
for G being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C st P2[C] holds
ex H being ManySortedFunction of F2(),C st
( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
H = K ) ) by A2;
A18: P2[F2()] by A3;
consider H being ManySortedFunction of F2(),A such that
A19: H is_homomorphism F2(),A and
A20: fi -hash = H ** (F3() -hash ) from BIRKHOFF:sch 3(A13, A15);
 H is_monomorphism F2(),A
proof
thus H is_homomorphism F2(),A by A19; :: according to MSUALG_3:def 11 :: thesis: H is "1-1"
now
let i be set ; :: thesis: ( i in the carrier of F1() implies H . i is one-to-one )
assume i in the carrier of F1() ; :: thesis: H . i is one-to-one
then reconsider s = i as SortSymbol of F1() ;
thus H . i is one-to-one :: thesis: verum
proof
let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a in dom (H . i) or not b in dom (H . i) or not (H . i) . a = (H . i) . b or a = b )
assume that
A21: a in dom (H . i) and
A22: b in dom (H . i) and
A23: (H . i) . a = (H . i) . b ; :: thesis: a = b
A24: for D being non-empty MSAlgebra of F1()
for E being strict non-empty MSSubAlgebra of D st P2[D] holds
P2[E]
proof
let D be non-empty MSAlgebra of F1(); :: thesis: for E being strict non-empty MSSubAlgebra of D st P2[D] holds
P2[E]
let E be strict non-empty MSSubAlgebra of D; :: thesis: ( P2[D] implies P2[E] )
assume A25: P2[D] ; :: thesis: P2[E]
now
let s be SortSymbol of F1(); :: thesis: for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra of F1() st P1[B] holds
B |= e ) holds
E |= e
let e be Element of (Equations F1()) . s; :: thesis: ( ( for B being non-empty MSAlgebra of F1() st P1[B] holds
B |= e ) implies E |= e )
assume for B being non-empty MSAlgebra of F1() st P1[B] holds
B |= e ; :: thesis: E |= e
then D |= e by A1, A25;
hence E |= e by EQUATION:33; :: thesis: verum
end;
hence P2[E] by A1; :: thesis: verum
end;
F3() -hash is_epimorphism FreeMSA (the carrier of F1() --> NAT ),F2() from BIRKHOFF:sch 6(A17, A18, A24);
 then A26: F3() -hash is "onto" by MSUALG_3:def 10;
A27: dom (H . s) = the Sorts of F2() . s by FUNCT_2:def 1
.= rng ((F3() -hash ) . s) by A26, MSUALG_3:def 3 ;
then consider t1 being set such that
A28: ( t1 in dom ((F3() -hash ) . s) & ((F3() -hash ) . s) . t1 = a ) by A21, FUNCT_1:def 5;
consider t2 being set such that
A29: ( t2 in dom ((F3() -hash ) . s) & ((F3() -hash ) . s) . t2 = b ) by A22, A27, FUNCT_1:def 5;
reconsider t1 = t1, t2 = t2 as Element of the Sorts of (TermAlg F1()) . s by A28, A29;
A30: ((fi -hash ) . s) . t1 = ((H . s) * ((F3() -hash ) . s)) . t1 by A20, MSUALG_3:2
.= (H . s) . a by A28, FUNCT_2:21
.= ((H . s) * ((F3() -hash ) . s)) . t2 by A23, A29, FUNCT_2:21
.= ((fi -hash ) . s) . t2 by A20, MSUALG_3:2 ;
A31: for C being non-empty MSAlgebra of F1()
for G being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C st P1[C] holds
ex H being ManySortedFunction of A,C st
( H is_homomorphism A,C & G = H ** fi )
proof
let C be non-empty MSAlgebra of F1(); :: thesis: for G being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C st P1[C] holds
ex H being ManySortedFunction of A,C st
( H is_homomorphism A,C & G = H ** fi )
let G be ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of C; :: thesis: ( P1[C] implies ex H being ManySortedFunction of A,C st
( H is_homomorphism A,C & G = H ** fi ) )
assume P1[C] ; :: thesis: ex H being ManySortedFunction of A,C st
( H is_homomorphism A,C & G = H ** fi )
then consider H being ManySortedFunction of A,C such that
A32: ( H is_homomorphism A,C & H ** fi = G ) and
for K being ManySortedFunction of A,C st K is_homomorphism A,C & K ** fi = G holds
H = K by A12;
take H ; :: thesis: ( H is_homomorphism A,C & G = H ** fi )
thus ( H is_homomorphism A,C & G = H ** fi ) by A32; :: thesis: verum
end;
set e = t1 '=' t2;
for B being non-empty MSAlgebra of F1() st P1[B] holds
B |= t1 '=' t2 from BIRKHOFF:sch 4(A30, A31);
 then A33: F2() |= t1 '=' t2 by A1, A3;
thus a = ((F3() -hash ) . s) . ((t1 '=' t2) `1 ) by A28, MCART_1:7
.= ((F3() -hash ) . s) . ((t1 '=' t2) `2 ) by A14, A33, EQUATION:def 5
.= b by A29, MCART_1:7 ; :: thesis: verum
end;
end;
hence H is "1-1" by MSUALG_3:1; :: thesis: verum
end;
then A34: F2(), Image H are_isomorphic by MSUALG_9:17;
P1[ Image H] by A5, A11;
hence P1[F2()] by A4, A34, MSUALG_3:17; :: thesis: verum