thus ex PC being MSAlgebra-Family of I,S st
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs ) :: thesis:

defpred S₁[ object , object ] means ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . $1 & Cs = C . $1 & $2 = product Cs );

let i be object ; :: thesis:
assume A2: i in I ; :: thesis:
then reconsider Ji = J . i as non empty set ;
reconsider Cs = C . i as MSAlgebra-Family of Ji,S by A2, Def3;
ex a being object st a = product Cs ;
then consider j being object such that
A3: ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & j = product Cs ) ;
reconsider j = j as object ;
take j = j; :: thesis:
thus S₁[i,j] by A3; :: thesis:

end;

consider PC being ManySortedSet of I such that
A4: for i being object st i in I holds
S₁[i,PC . i] from PBOOLE:sch 3(A1);

let i be object ; :: thesis:
assume i in I ; :: thesis:
then ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs ) by A4;
hence PC . i is non-empty MSAlgebra over S ; :: thesis:

end;

then reconsider PC = PC as MSAlgebra-Family of I,S by PRALG_2:def 5;
take PC ; :: thesis:
thus for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs ) by A4; :: thesis:

end;