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

P_{1}[B]
by A2;

set T = the strict non-empty finitely-generated MSSubAlgebra of F_{2}();

set CC = { C where C is Element of MSSub F_{2}() : ex R being strict non-empty finitely-generated MSSubAlgebra of F_{2}() st R = C } ;

the strict non-empty finitely-generated MSSubAlgebra of F_{2}() in MSSub F_{2}()
by MSUALG_2:def 19;

then the strict non-empty finitely-generated MSSubAlgebra of F_{2}() in { C where C is Element of MSSub F_{2}() : ex R being strict non-empty finitely-generated MSSubAlgebra of F_{2}() st R = C }
;

then reconsider CC = { C where C is Element of MSSub F_{2}() : ex R being strict non-empty finitely-generated MSSubAlgebra of F_{2}() st R = C } as non empty set ;

defpred S_{1}[ object , object ] means $1 = $2;

A7: for c being object st c in CC holds

ex j being object st S_{1}[c,j]
;

consider FF being ManySortedSet of CC such that

A8: for c being object st c in CC holds

S_{1}[c,FF . c]
from PBOOLE:sch 3(A7);

FF is MSAlgebra-Family of CC,F_{1}()
_{1}() ;

consider prSOR being strict non-empty MSSubAlgebra of product FF such that

A10: ex BA being ManySortedFunction of prSOR,F_{2}() st BA is_epimorphism prSOR,F_{2}()
by A8, EQUATION:27;

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

for i being set st i in CC holds

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

( A = FF . i & P_{1}[A] )
_{1}[prSOR]
by A3, A5;

thus P_{1}[F_{2}()]
from BIRKHOFF:sch 8(A10, A16, A6, A11); :: thesis: verum

P

set T = the strict non-empty finitely-generated MSSubAlgebra of F

set CC = { C where C is Element of MSSub F

the strict non-empty finitely-generated MSSubAlgebra of F

then the strict non-empty finitely-generated MSSubAlgebra of F

then reconsider CC = { C where C is Element of MSSub F

defpred S

A7: for c being object st c in CC holds

ex j being object st S

consider FF being ManySortedSet of CC such that

A8: for c being object st c in CC holds

S

FF is MSAlgebra-Family of CC,F

proof

then reconsider FF = FF as MSAlgebra-Family of CC,F
let c be object ; :: according to PRALG_2:def 5 :: thesis: ( not c in CC or FF . c is MSAlgebra over F_{1}() )

assume A9: c in CC ; :: thesis: FF . c is MSAlgebra over F_{1}()

then ex Q being Element of MSSub F_{2}() st

( c = Q & ex R being strict non-empty finitely-generated MSSubAlgebra of F_{2}() st R = Q )
;

hence FF . c is MSAlgebra over F_{1}()
by A8, A9; :: thesis: verum

end;assume A9: c in CC ; :: thesis: FF . c is MSAlgebra over F

then ex Q being Element of MSSub F

( c = Q & ex R being strict non-empty finitely-generated MSSubAlgebra of F

hence FF . c is MSAlgebra over F

consider prSOR being strict non-empty MSSubAlgebra of product FF such that

A10: ex BA being ManySortedFunction of prSOR,F

A11: for A being non-empty MSAlgebra over F

for R being MSCongruence of A st P

P

for i being set st i in CC holds

ex A being MSAlgebra over F

( A = FF . i & P

proof

then A16:
P
let i be set ; :: thesis: ( i in CC implies ex A being MSAlgebra over F_{1}() st

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

assume A12: i in CC ; :: thesis: ex A being MSAlgebra over F_{1}() st

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

then consider Q being Element of MSSub F_{2}() such that

A13: i = Q and

A14: ex R being strict non-empty finitely-generated MSSubAlgebra of F_{2}() st R = Q
;

consider R being strict non-empty finitely-generated MSSubAlgebra of F_{2}() such that

A15: R = Q by A14;

take R ; :: thesis: ( R = FF . i & P_{1}[R] )

thus ( R = FF . i & P_{1}[R] )
by A1, A8, A12, A13, A15; :: thesis: verum

end;( A = FF . i & P

assume A12: i in CC ; :: thesis: ex A being MSAlgebra over F

( A = FF . i & P

then consider Q being Element of MSSub F

A13: i = Q and

A14: ex R being strict non-empty finitely-generated MSSubAlgebra of F

consider R being strict non-empty finitely-generated MSSubAlgebra of F

A15: R = Q by A14;

take R ; :: thesis: ( R = FF . i & P

thus ( R = FF . i & P

thus P