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

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

set I = the carrier of F_{1}();

defpred S_{1}[ object , object ] means ex s being SortSymbol of F_{1}() st

( $1 = s & $2 = { e where e is Element of (Equations F_{1}()) . s : for A being non-empty MSAlgebra over F_{1}() st P_{1}[A] holds

A |= e } );

_{1}() such that

A8: for i being object st i in the carrier of F_{1}() holds

S_{1}[i,E . i]
from PBOOLE:sch 3(A6);

E is ManySortedSubset of Equations F_{1}()
_{1}() ;

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

P_{1}[B]
by A1;

defpred S_{2}[ MSAlgebra over F_{1}()] means $1 |= E;

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

( S_{2}[D] iff for s being SortSymbol of F_{1}()

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

M |= e ) holds

D |= e )_{1}()

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

S_{2}[B]
by EQUATION:32;

A18: 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 & S_{2}[A] ) ) holds

S_{2}[ product F]
by EQUATION:38;

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

S_{2}[B]
by EQUATION:34;

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

A20: S_{2}[K]
and

A21: 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 S_{2}[B] holds

ex H being ManySortedFunction of K,B st

( H is_homomorphism K,B & H ** F = G & ( for W being ManySortedFunction of K,B st W is_homomorphism K,B & W ** F = G holds

H = W ) ) from BIRKHOFF:sch 2(A19, A17, A18);

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

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

ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & G = H ** F )

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 A4;

take E ; :: thesis: for A being non-empty MSAlgebra over F_{1}() holds

( P_{1}[A] iff A |= E )

let A be non-empty MSAlgebra over F_{1}(); :: thesis: ( P_{1}[A] iff A |= E )

_{1}[A]

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

for R being MSCongruence of A st P_{1}[A] holds

P_{1}[ QuotMSAlg (A,R)]
by A3;

A31: S_{2}[K]
by A20;

A32: P_{1}[K]
from BIRKHOFF:sch 11(A12, A21, A31, A11, A5, A23);

A33: for B being strict non-empty finitely-generated MSSubAlgebra of A holds P_{1}[B]
_{1}[A]
from BIRKHOFF:sch 9(A33, A11, A5, A30, A23); :: thesis: verum

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

P

set XX = the carrier of F

set I = the carrier of F

defpred S

( $1 = s & $2 = { e where e is Element of (Equations F

A |= e } );

A6: now :: thesis: for w being object st w in the carrier of F_{1}() holds

ex d being object st S_{1}[w,d]

consider E being ManySortedSet of the carrier of Fex d being object st S

let w be object ; :: thesis: ( w in the carrier of F_{1}() implies ex d being object st S_{1}[w,d] )

assume w in the carrier of F_{1}()
; :: thesis: ex d being object st S_{1}[w,d]

then consider s being SortSymbol of F_{1}() such that

A7: s = w ;

reconsider d = { e where e is Element of (Equations F_{1}()) . s : for A being non-empty MSAlgebra over F_{1}() st P_{1}[A] holds

A |= e } as object ;

take d = d; :: thesis: S_{1}[w,d]

thus S_{1}[w,d]
by A7; :: thesis: verum

end;assume w in the carrier of F

then consider s being SortSymbol of F

A7: s = w ;

reconsider d = { e where e is Element of (Equations F

A |= e } as object ;

take d = d; :: thesis: S

thus S

A8: for i being object st i in the carrier of F

S

E is ManySortedSubset of Equations F

proof

then reconsider E = E as EqualSet of F
let j be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not j in the carrier of F_{1}() or E . j c= (Equations F_{1}()) . j )

assume j in the carrier of F_{1}()
; :: thesis: E . j c= (Equations F_{1}()) . j

then consider s being SortSymbol of F_{1}() such that

A9: j = s and

A10: E . j = { e where e is Element of (Equations F_{1}()) . s : for A being non-empty MSAlgebra over F_{1}() st P_{1}[A] holds

A |= e } by A8;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in E . j or q in (Equations F_{1}()) . j )

assume q in E . j ; :: thesis: q in (Equations F_{1}()) . j

then ex z being Element of (Equations F_{1}()) . s st

( q = z & ( for A being non-empty MSAlgebra over F_{1}() st P_{1}[A] holds

A |= z ) ) by A10;

hence q in (Equations F_{1}()) . j
by A9; :: thesis: verum

end;assume j in the carrier of F

then consider s being SortSymbol of F

A9: j = s and

A10: E . j = { e where e is Element of (Equations F

A |= e } by A8;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in E . j or q in (Equations F

assume q in E . j ; :: thesis: q in (Equations F

then ex z being Element of (Equations F

( q = z & ( for A being non-empty MSAlgebra over F

A |= z ) ) by A10;

hence q in (Equations F

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

P

defpred S

A12: for D being non-empty MSAlgebra over F

( S

for e being Element of (Equations F

M |= e ) holds

D |= e )

proof

A17:
for A being non-empty MSAlgebra over F
let D be non-empty MSAlgebra over F_{1}(); :: thesis: ( S_{2}[D] iff for s being SortSymbol of F_{1}()

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

M |= e ) holds

D |= e )

thus ( S_{2}[D] implies 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

D |= e ) :: thesis: ( ( for s being SortSymbol of F_{1}()

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

M |= e ) holds

D |= e ) implies S_{2}[D] )_{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

D |= e ; :: thesis: S_{2}[D]

let s be SortSymbol of F_{1}(); :: according to EQUATION:def 6 :: thesis: for b_{1} being Element of (Equations F_{1}()) . s holds

( not b_{1} in E . s or D |= b_{1} )

let e be Element of (Equations F_{1}()) . s; :: thesis: ( not e in E . s or D |= e )

assume A16: e in E . s ; :: thesis: D |= e

S_{1}[s,E . s]
by A8;

then ex f being Element of (Equations F_{1}()) . s st

( e = f & ( for A being non-empty MSAlgebra over F_{1}() st P_{1}[A] holds

A |= f ) ) by A16;

hence D |= e by A15; :: thesis: verum

end;for e being Element of (Equations F

M |= e ) holds

D |= e )

thus ( S

for e being Element of (Equations F

B |= e ) holds

D |= e ) :: thesis: ( ( for s being SortSymbol of F

for e being Element of (Equations F

M |= e ) holds

D |= e ) implies S

proof

assume A15:
for s being SortSymbol of F
assume A13:
S_{2}[D]
; :: thesis: 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

D |= e

let s be SortSymbol of F_{1}(); :: thesis: 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

D |= e

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

B |= e ) implies D |= e )

assume A14: for B being non-empty MSAlgebra over F_{1}() st P_{1}[B] holds

B |= e ; :: thesis: D |= e

S_{1}[s,E . s]
by A8;

then e in E . s by A14;

hence D |= e by A13, EQUATION:def 6; :: thesis: verum

end;for e being Element of (Equations F

B |= e ) holds

D |= e

let s be SortSymbol of F

B |= e ) holds

D |= e

let e be Element of (Equations F

B |= e ) implies D |= e )

assume A14: for B being non-empty MSAlgebra over F

B |= e ; :: thesis: D |= e

S

then e in E . s by A14;

hence D |= e by A13, EQUATION:def 6; :: thesis: verum

for e being Element of (Equations F

B |= e ) holds

D |= e ; :: thesis: S

let s be SortSymbol of F

( not b

let e be Element of (Equations F

assume A16: e in E . s ; :: thesis: D |= e

S

then ex f being Element of (Equations F

( e = f & ( for A being non-empty MSAlgebra over F

A |= f ) ) by A16;

hence D |= e by A15; :: thesis: verum

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

S

A18: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & S

S

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

S

consider K being strict non-empty MSAlgebra over F

A20: S

A21: for B being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of K,B st

( H is_homomorphism K,B & H ** F = G & ( for W being ManySortedFunction of K,B st W is_homomorphism K,B & W ** F = G holds

H = W ) ) from BIRKHOFF:sch 2(A19, A17, A18);

A22: for M being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & G = H ** F )

proof

A23:
for I being set
let M be non-empty MSAlgebra over F_{1}(); :: thesis: for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of M st S_{2}[M] holds

ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & G = H ** F )

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

( H is_homomorphism K,M & G = H ** F ) )

assume S_{2}[M]
; :: thesis: ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & G = H ** F )

then ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & H ** F = G & ( for W being ManySortedFunction of K,M st W is_homomorphism K,M & W ** F = G holds

H = W ) ) by A21;

hence ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & H ** F = G ) ; :: thesis: verum

end;ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & G = H ** F )

let G be ManySortedFunction of the carrier of F

( H is_homomorphism K,M & G = H ** F ) )

assume S

( H is_homomorphism K,M & G = H ** F )

then ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & H ** F = G & ( for W being ManySortedFunction of K,M st W is_homomorphism K,M & W ** F = G holds

H = W ) ) by A21;

hence ex H being ManySortedFunction of K,M st

( H is_homomorphism K,M & H ** F = G ) ; :: thesis: verum

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

take E ; :: thesis: for A being non-empty MSAlgebra over F

( P

let A be non-empty MSAlgebra over F

hereby :: thesis: ( A |= E implies P_{1}[A] )

assume A29:
A |= E
; :: thesis: Passume A24:
P_{1}[A]
; :: thesis: A |= E

thus A |= E :: thesis: verum

end;thus A |= E :: thesis: verum

proof

let s1 be SortSymbol of F_{1}(); :: according to EQUATION:def 6 :: thesis: for b_{1} being Element of (Equations F_{1}()) . s1 holds

( not b_{1} in E . s1 or A |= b_{1} )

A25: S_{1}[s1,E . s1]
by A8;

let e be Element of (Equations F_{1}()) . s1; :: thesis: ( not e in E . s1 or A |= e )

assume e in E . s1 ; :: thesis: A |= e

then consider x being Element of (Equations F_{1}()) . s1 such that

A26: e = x and

A27: for A being non-empty MSAlgebra over F_{1}() st P_{1}[A] holds

A |= x by A25;

A28: A |= x by A24, A27;

let h be ManySortedFunction of (TermAlg F_{1}()),A; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg F_{1}(),A or (h . s1) . (e `1) = (h . s1) . (e `2) )

assume h is_homomorphism TermAlg F_{1}(),A
; :: thesis: (h . s1) . (e `1) = (h . s1) . (e `2)

hence (h . s1) . (e `1) = (h . s1) . (e `2) by A26, A28; :: thesis: verum

end;( not b

A25: S

let e be Element of (Equations F

assume e in E . s1 ; :: thesis: A |= e

then consider x being Element of (Equations F

A26: e = x and

A27: for A being non-empty MSAlgebra over F

A |= x by A25;

A28: A |= x by A24, A27;

let h be ManySortedFunction of (TermAlg F

assume h is_homomorphism TermAlg F

hence (h . s1) . (e `1) = (h . s1) . (e `2) by A26, A28; :: thesis: verum

A30: for A being non-empty MSAlgebra over F

for R being MSCongruence of A st P

P

A31: S

A32: P

A33: for B being strict non-empty finitely-generated MSSubAlgebra of A holds P

proof

thus
P
let B be strict non-empty finitely-generated MSSubAlgebra of A; :: thesis: P_{1}[B]

A34: S_{2}[B]
by A29, EQUATION:32;

thus P_{1}[B]
from BIRKHOFF:sch 7(A34, A32, A22, A11, A30); :: thesis: verum

end;A34: S

thus P