A6: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] by A2;
set T = the strict non-empty finitely-generated MSSubAlgebra of F₂();
set CC = { C where C is Element of MSSub F₂() : ex R being strict non-empty finitely-generated MSSubAlgebra of F₂() st R = C } ;
the strict non-empty finitely-generated MSSubAlgebra of F₂() in MSSub F₂() by MSUALG_2:def 19;
then the strict non-empty finitely-generated MSSubAlgebra of F₂() in { C where C is Element of MSSub F₂() : ex R being strict non-empty finitely-generated MSSubAlgebra of F₂() st R = C } ;
then reconsider CC = { C where C is Element of MSSub F₂() : ex R being strict non-empty finitely-generated MSSubAlgebra of F₂() st R = C } as non empty set ;
defpred S₁[ object , object ] means $1 = $2;
A7: for c being object st c in CC holds
ex j being object st S₁[c,j] ;
consider FF being ManySortedSet of CC such that
A8: for c being object st c in CC holds
S₁[c,FF . c] from PBOOLE:sch 3(A7);
FF is MSAlgebra-Family of CC,F₁()

proof

let c be object ; :: according to PRALG_2:def 5 :: thesis: ( not c in CC or FF . c is MSAlgebra over F₁() )
assume A9: c in CC ; :: thesis: FF . c is MSAlgebra over F₁()
then ex Q being Element of MSSub F₂() st
( c = Q & ex R being strict non-empty finitely-generated MSSubAlgebra of F₂() st R = Q ) ;
hence FF . c is MSAlgebra over F₁() by A8, A9; :: thesis: verum

end;

then reconsider FF = FF as MSAlgebra-Family of CC,F₁() ;
consider prSOR being strict non-empty MSSubAlgebra of product FF such that
A10: ex BA being ManySortedFunction of prSOR,F₂() st BA is_epimorphism prSOR,F₂() by A8, EQUATION:27;
A11: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)] by A4;
for i being set st i in CC holds
ex A being MSAlgebra over F₁() st
( A = FF . i & P₁[A] )

proof

let i be set ; :: thesis: ( i in CC implies ex A being MSAlgebra over F₁() st
( A = FF . i & P₁[A] ) )
assume A12: i in CC ; :: thesis: ex A being MSAlgebra over F₁() st
( A = FF . i & P₁[A] )
then consider Q being Element of MSSub F₂() such that
A13: i = Q and
A14: ex R being strict non-empty finitely-generated MSSubAlgebra of F₂() st R = Q ;
consider R being strict non-empty finitely-generated MSSubAlgebra of F₂() such that
A15: R = Q by A14;
take R ; :: thesis: ( R = FF . i & P₁[R] )
thus ( R = FF . i & P₁[R] ) by A1, A8, A12, A13, A15; :: thesis: verum

end;

then A16: P₁[prSOR] by A3, A5;
thus P₁[F₂()] from BIRKHOFF:sch 8(A10, A16, A6, A11); :: thesis: verum