let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
let U0 be non-empty MSAlgebra over S; :: thesis: for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
let A, B be strict non-empty finitely-generated MSSubAlgebra of U0; :: thesis: ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
len <%A,B%> = 2 by AFINSQ_1:38;
then dom <%A,B%> = {0,1} by CARD_1:50;
then reconsider F = <%A,B%> as ManySortedSet of {0,1} by RELAT_1:def 18, PARTFUN1:def 2;
A1: F . 1 = B ;
A2: F . 0 = A ;
F is MSAlgebra-Family of {0,1},S

proof

let i be object ; :: according to PRALG_2:def 5 :: thesis: ( not i in {0,1} or F . i is MSAlgebra over S )
assume i in {0,1} ; :: thesis: F . i is MSAlgebra over S
hence F . i is MSAlgebra over S by A1, TARSKI:def 2, A2; :: thesis: verum

end;

then reconsider F = F as MSAlgebra-Family of {0,1},S ;
for i being Element of {0,1} ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

proof

let i be Element of {0,1}; :: thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

per cases ( i = 0 or i = 1 ) by TARSKI:def 2;

suppose A3: i = 0 ; :: thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

take A ; :: thesis: A = F . i
thus A = F . i by A3; :: thesis: verum

end;

suppose A4: i = 1 ; :: thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

take B ; :: thesis: B = F . i
thus B = F . i by A4; :: thesis: verum

end;

end;

end;

then consider M being strict non-empty finitely-generated MSSubAlgebra of U0 such that
A5: for i being Element of {0,1} holds F . i is MSSubAlgebra of M by Th25;
take M ; :: thesis: ( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
0 in {0,1} by TARSKI:def 2;
hence A is MSSubAlgebra of M by A5, A2; :: thesis: B is MSSubAlgebra of M
1 in {0,1} by TARSKI:def 2;
hence B is MSSubAlgebra of M by A5, A1; :: thesis: verum