A5: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] by A2;
set XX = the carrier of F1() --> NAT;
set I = the carrier of F1();
defpred S1[ object , object ] means ex s being SortSymbol of F1() st
( $1 = s & $2 = { e where e is Element of (Equations F1()) . s : for A being non-empty MSAlgebra over F1() st P1[A] holds
A |= e } );
A6: now :: thesis: for w being object st w in the carrier of F1() holds
ex d being object st S1[w,d]
let w be object ; :: thesis: ( w in the carrier of F1() implies ex d being object st S1[w,d] )
assume w in the carrier of F1() ; :: thesis: ex d being object st S1[w,d]
then consider s being SortSymbol of F1() such that
A7: s = w ;
reconsider d = { e where e is Element of (Equations F1()) . s : for A being non-empty MSAlgebra over F1() st P1[A] holds
A |= e } as object ;
take d = d; :: thesis: S1[w,d]
thus S1[w,d] by A7; :: thesis: verum
end;
consider E being ManySortedSet of the carrier of F1() such that
A8: for i being object st i in the carrier of F1() holds
S1[i,E . i] from PBOOLE:sch 3(A6);
 E is ManySortedSubset of Equations F1()
proof
let j be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not j in the carrier of F1() or E . j c= (Equations F1()) . j )
assume j in the carrier of F1() ; :: thesis: E . j c= (Equations F1()) . j
then consider s being SortSymbol of F1() such that
A9: j = s and
A10: E . j = { e where e is Element of (Equations F1()) . s : for A being non-empty MSAlgebra over F1() st P1[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 F1()) . j )
assume q in E . j ; :: thesis: q in (Equations F1()) . j
then ex z being Element of (Equations F1()) . s st
( q = z & ( for A being non-empty MSAlgebra over F1() st P1[A] holds
A |= z ) ) by A10;
hence q in (Equations F1()) . j by A9; :: thesis: verum
end;
then reconsider E = E as EqualSet of F1() ;
A11: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] by A1;
defpred S2[ MSAlgebra over F1()] means $1 |= E;
A12: for D being non-empty MSAlgebra over F1() holds
( S2[D] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for M being non-empty MSAlgebra over F1() st P1[M] holds
M |= e ) holds
D |= e )
proof
let D be non-empty MSAlgebra over F1(); :: thesis: ( S2[D] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for M being non-empty MSAlgebra over F1() st P1[M] holds
M |= e ) holds
D |= e )
thus ( S2[D] implies 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
D |= e ) :: thesis: ( ( for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for M being non-empty MSAlgebra over F1() st P1[M] holds
M |= e ) holds
D |= e ) implies S2[D] )
proof
assume A13: S2[D] ; :: thesis: 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
D |= e
let s be SortSymbol of F1(); :: thesis: for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) holds
D |= e
let e be Element of (Equations F1()) . s; :: thesis: ( ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) implies D |= e )
assume A14: for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ; :: thesis: D |= e
S1[s,E . s] by A8;
then e in E . s by A14;
hence D |= e by A13, EQUATION:def 6; :: thesis: verum
end;
assume A15: 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
D |= e ; :: thesis: S2[D]
let s be SortSymbol of F1(); :: according to EQUATION:def 6 :: thesis: for b1 being Element of (Equations F1()) . s holds
( not b1 in E . s or D |= b1 )
let e be Element of (Equations F1()) . s; :: thesis: ( not e in E . s or D |= e )
assume A16: e in E . s ; :: thesis: D |= e
S1[s,E . s] by A8;
then ex f being Element of (Equations F1()) . s st
( e = f & ( for A being non-empty MSAlgebra over F1() st P1[A] holds
A |= f ) ) by A16;
hence D |= e by A15; :: thesis: verum
end;
A17: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st S2[A] holds
S2[B] by EQUATION:32;
A18: 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 & S2[A] ) ) holds
S2[ product F] by EQUATION:38;
A19: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & S2[A] holds
S2[B] by EQUATION:34;
consider K being strict non-empty MSAlgebra over F1(), F being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of K such that
A20: S2[K] and
A21: for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of B st S2[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 F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of M st S2[M] holds
ex H being ManySortedFunction of K,M st
( H is_homomorphism K,M & G = H ** F )
proof
let M be non-empty MSAlgebra over F1(); :: thesis: for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of M st S2[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 F1() --> NAT, the Sorts of M; :: thesis: ( S2[M] implies ex H being ManySortedFunction of K,M st
( H is_homomorphism K,M & G = H ** F ) )
assume S2[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;
A23: 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 A4;
take E ; :: thesis: for A being non-empty MSAlgebra over F1() holds
( P1[A] iff A |= E )
let A be non-empty MSAlgebra over F1(); :: thesis: ( P1[A] iff A |= E )
hereby :: thesis: ( A |= E implies P1[A] )
assume A24: P1[A] ; :: thesis: A |= E
thus A |= E :: thesis: verum
proof
let s1 be SortSymbol of F1(); :: according to EQUATION:def 6 :: thesis: for b1 being Element of (Equations F1()) . s1 holds
( not b1 in E . s1 or A |= b1 )
A25: S1[s1,E . s1] by A8;
let e be Element of (Equations F1()) . 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 F1()) . s1 such that
A26: e = x and
A27: for A being non-empty MSAlgebra over F1() st P1[A] holds
A |= x by A25;
A28: A |= x by A24, A27;
let h be ManySortedFunction of (TermAlg F1()),A; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg F1(),A or (h . s1) . (e `1) = (h . s1) . (e `2) )
assume h is_homomorphism TermAlg F1(),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;
end;
assume A29: A |= E ; :: thesis: P1[A]
A30: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)] by A3;
A31: S2[K] by A20;
A32: P1[K] from BIRKHOFF:sch 11(A12, A21, A31, A11, A5, A23);
A33: for B being strict non-empty finitely-generated MSSubAlgebra of A holds P1[B]
proof
let B be strict non-empty finitely-generated MSSubAlgebra of A; :: thesis: P1[B]
A34: S2[B] by A29, EQUATION:32;
thus P1[B] from BIRKHOFF:sch 7(A34, A32, A22, A11, A30); :: thesis: verum
end;
thus P1[A] from BIRKHOFF:sch 9(A33, A11, A5, A30, A23); :: thesis: verum