A7:
for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]
by A6;

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

A8: 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 A5;

A9: for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
by A4;

consider A being strict non-empty MSAlgebra over F_{1}(), fi being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of A such that

A10: P_{1}[A]
and

A11: for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of B st P_{1}[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 F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{2}[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 A2;

A13: 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_{2}[C] holds

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

( h is_homomorphism F_{2}(),C & G = h ** F_{3}() )
_{2}[F_{2}()]
by A3;

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

( P_{2}[A] iff for s being SortSymbol of F_{1}()

for e being Element of (Equations F_{1}()) . s st ( for B being non-empty MSAlgebra over F_{1}() st P_{1}[B] holds

B |= e ) holds

A |= e ) by A1;

A18: P_{2}[A]
from BIRKHOFF:sch 10(A17, A10);

consider H being ManySortedFunction of F_{2}(),A such that

A19: H is_homomorphism F_{2}(),A
and

A20: fi -hash = H ** (F_{3}() -hash)
from BIRKHOFF:sch 3(A18, A13);

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

then H is_monomorphism F_{2}(),A
by A19, MSUALG_3:def 9;

then A38: F_{2}(), Image H are_isomorphic
by MSUALG_9:16;

P_{1}[ Image H]
by A5, A10;

hence P_{1}[F_{2}()]
by A4, A38, MSUALG_3:17; :: thesis: verum

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

set V = the carrier of F

A8: for A being non-empty MSAlgebra over F

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

P

A9: for A, B being non-empty MSAlgebra over F

P

consider A being strict non-empty MSAlgebra over F

A10: P

A11: for B being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

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 F

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of F

( H is_homomorphism F

H = K ) ) by A2;

A13: 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

proof

A16:
P
let C be non-empty MSAlgebra over F_{1}(); :: thesis: for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{2}[C] holds

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

( h is_homomorphism F_{2}(),C & G = h ** F_{3}() )

let G be ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C; :: thesis: ( P_{2}[C] implies ex h being ManySortedFunction of F_{2}(),C st

( h is_homomorphism F_{2}(),C & G = h ** F_{3}() ) )

assume P_{2}[C]
; :: thesis: ex h being ManySortedFunction of F_{2}(),C st

( h is_homomorphism F_{2}(),C & G = h ** F_{3}() )

then consider h being ManySortedFunction of F_{2}(),C such that

A14: h is_homomorphism F_{2}(),C
and

A15: G = h ** F_{3}()
and

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

h = K by A2;

take h ; :: thesis: ( h is_homomorphism F_{2}(),C & G = h ** F_{3}() )

thus ( h is_homomorphism F_{2}(),C & G = h ** F_{3}() )
by A14, A15; :: thesis: verum

end;ex h being ManySortedFunction of F

( h is_homomorphism F

let G be ManySortedFunction of the carrier of F

( h is_homomorphism F

assume P

( h is_homomorphism F

then consider h being ManySortedFunction of F

A14: h is_homomorphism F

A15: G = h ** F

for K being ManySortedFunction of F

h = K by A2;

take h ; :: thesis: ( h is_homomorphism F

thus ( h is_homomorphism F

A17: for A being non-empty MSAlgebra over F

( P

for e being Element of (Equations F

B |= e ) holds

A |= e ) by A1;

A18: P

consider H being ManySortedFunction of F

A19: H is_homomorphism F

A20: fi -hash = H ** (F

A21: F

now :: thesis: for i being set st i in the carrier of F_{1}() holds

H . i is one-to-one

then
H is "1-1"
by MSUALG_3:1;H . i is one-to-one

let i be set ; :: thesis: ( i in the carrier of F_{1}() implies H . i is one-to-one )

assume i in the carrier of F_{1}()
; :: thesis: H . i is one-to-one

then reconsider s = i as SortSymbol of F_{1}() ;

thus H . i is one-to-one :: thesis: verum

end;assume i in the carrier of F

then reconsider s = i as SortSymbol of F

thus H . i is one-to-one :: thesis: verum

proof

A22:
for D being non-empty MSAlgebra over F_{1}()

for E being strict non-empty MSSubAlgebra of D st P_{2}[D] holds

P_{2}[E]
_{3}() -hash is_epimorphism FreeMSA ( the carrier of F_{1}() --> NAT),F_{2}()
from BIRKHOFF:sch 6(A12, A16, A22);

then A24: F_{3}() -hash is "onto"
by MSUALG_3:def 8;

A25: 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 A,C st

( H is_homomorphism A,C & G = H ** fi )

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 F_{2}() . s
by FUNCT_2:def 1

.= rng ((F_{3}() -hash) . s)
by A24, MSUALG_3:def 3
;

then consider t1 being object such that

A32: t1 in dom ((F_{3}() -hash) . s)
and

A33: ((F_{3}() -hash) . s) . t1 = a
by A28, FUNCT_1:def 3;

consider t2 being object such that

A34: t2 in dom ((F_{3}() -hash) . s)
and

A35: ((F_{3}() -hash) . s) . t2 = b
by A29, A31, FUNCT_1:def 3;

reconsider t1 = t1, t2 = t2 as Element of the Sorts of (TermAlg F_{1}()) . s by A32, A34;

set e = t1 '=' t2;

A36: ((fi -hash) . s) . t1 = ((H . s) * ((F_{3}() -hash) . s)) . t1
by A20, MSUALG_3:2

.= (H . s) . a by A33, FUNCT_2:15

.= ((H . s) * ((F_{3}() -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 F_{1}() st P_{1}[B] holds

B |= t1 '=' t2 from BIRKHOFF:sch 4(A36, A25);

then A37: F_{2}() |= t1 '=' t2
by A1, A3;

thus a = ((F_{3}() -hash) . s) . ((t1 '=' t2) `1)
by A33

.= ((F_{3}() -hash) . s) . ((t1 '=' t2) `2)
by A21, A37

.= b by A35 ; :: thesis: verum

end;for E being strict non-empty MSSubAlgebra of D st P

P

proof

F
let D be non-empty MSAlgebra over F_{1}(); :: thesis: for E being strict non-empty MSSubAlgebra of D st P_{2}[D] holds

P_{2}[E]

let E be strict non-empty MSSubAlgebra of D; :: thesis: ( P_{2}[D] implies P_{2}[E] )

assume A23: P_{2}[D]
; :: thesis: P_{2}[E]

for s being SortSymbol of F_{1}()

for e being Element of (Equations F_{1}()) . s st ( for B being non-empty MSAlgebra over F_{1}() st P_{1}[B] holds

B |= e ) holds

E |= e by A1, A23, EQUATION:31;

hence P_{2}[E]
by A1; :: thesis: verum

end;P

let E be strict non-empty MSSubAlgebra of D; :: thesis: ( P

assume A23: P

for s being SortSymbol of F

for e being Element of (Equations F

B |= e ) holds

E |= e by A1, A23, EQUATION:31;

hence P

then A24: F

A25: for C being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of A,C st

( H is_homomorphism A,C & G = H ** fi )

proof

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 )
let C be non-empty MSAlgebra over F_{1}(); :: thesis: 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 A,C st

( H is_homomorphism A,C & G = H ** fi )

let G be ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C; :: thesis: ( P_{1}[C] implies ex H being ManySortedFunction of A,C st

( H is_homomorphism A,C & G = H ** fi ) )

assume P_{1}[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;ex H being ManySortedFunction of A,C st

( H is_homomorphism A,C & G = H ** fi )

let G be ManySortedFunction of the carrier of F

( H is_homomorphism A,C & G = H ** fi ) )

assume P

( 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

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 F

.= rng ((F

then consider t1 being object such that

A32: t1 in dom ((F

A33: ((F

consider t2 being object such that

A34: t2 in dom ((F

A35: ((F

reconsider t1 = t1, t2 = t2 as Element of the Sorts of (TermAlg F

set e = t1 '=' t2;

A36: ((fi -hash) . s) . t1 = ((H . s) * ((F

.= (H . s) . a by A33, FUNCT_2:15

.= ((H . s) * ((F

.= ((fi -hash) . s) . t2 by A20, MSUALG_3:2 ;

for B being non-empty MSAlgebra over F

B |= t1 '=' t2 from BIRKHOFF:sch 4(A36, A25);

then A37: F

thus a = ((F

.= ((F

.= b by A35 ; :: thesis: verum

then H is_monomorphism F

then A38: F

P

hence P