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