A6: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] by A2;
set T = the strict non-empty finitely-generated MSSubAlgebra of F2();
set CC = { C where C is Element of MSSub F2() : ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = C } ;
the strict non-empty finitely-generated MSSubAlgebra of F2() in MSSub F2() by MSUALG_2:def 19;
then the strict non-empty finitely-generated MSSubAlgebra of F2() in { C where C is Element of MSSub F2() : ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = C } ;
then reconsider CC = { C where C is Element of MSSub F2() : ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = C } as non empty set ;
defpred S1[ object , object ] means \$1 = \$2;
A7: for c being object st c in CC holds
ex j being object st S1[c,j] ;
consider FF being ManySortedSet of CC such that
A8: for c being object st c in CC holds
S1[c,FF . c] from FF is MSAlgebra-Family of CC,F1()
proof
let c be object ; :: according to PRALG_2:def 5 :: thesis: ( not c in CC or FF . c is MSAlgebra over F1() )
assume A9: c in CC ; :: thesis: FF . c is MSAlgebra over F1()
then ex Q being Element of MSSub F2() st
( c = Q & ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = Q ) ;
hence FF . c is MSAlgebra over F1() by A8, A9; :: thesis: verum
end;
then reconsider FF = FF as MSAlgebra-Family of CC,F1() ;
consider prSOR being strict non-empty MSSubAlgebra of product FF such that
A10: ex BA being ManySortedFunction of prSOR,F2() st BA is_epimorphism prSOR,F2() by ;
A11: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)] by A4;
for i being set st i in CC holds
ex A being MSAlgebra over F1() st
( A = FF . i & P1[A] )
proof
let i be set ; :: thesis: ( i in CC implies ex A being MSAlgebra over F1() st
( A = FF . i & P1[A] ) )

assume A12: i in CC ; :: thesis: ex A being MSAlgebra over F1() st
( A = FF . i & P1[A] )

then consider Q being Element of MSSub F2() such that
A13: i = Q and
A14: ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = Q ;
consider R being strict non-empty finitely-generated MSSubAlgebra of F2() such that
A15: R = Q by A14;
take R ; :: thesis: ( R = FF . i & P1[R] )
thus ( R = FF . i & P1[R] ) by A1, A8, A12, A13, A15; :: thesis: verum
end;
then A16: P1[prSOR] by A3, A5;
thus P1[F2()] from BIRKHOFF:sch 8(A10, A16, A6, A11); :: thesis: verum