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 } );
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()
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 )
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();
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;
( S2[M] implies ex H being ManySortedFunction of K,M st
( H is_homomorphism K,M & G = H ** F ) )
assume
S2[
M]
;
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 )
;
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
; for A being non-empty MSAlgebra over F1() holds
( P1[A] iff A |= E )
let A be non-empty MSAlgebra over F1(); ( P1[A] iff A |= E )
hereby ( A |= E implies P1[A] )
assume A24:
P1[
A]
;
A |= Ethus
A |= E
verum
end;
assume A29:
A |= E
; 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]
thus
P1[A]
from BIRKHOFF:sch 9(A33, A11, A5, A30, A23); verum