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: verum

proof

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 );

A1: now :: thesis: for i being object st i in I holds
ex j being object st S₁[i,j]

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume A2: i in I ; :: thesis: ex j being object st S₁[i,j]
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: S₁[i,j]
thus S₁[i,j] by A3; :: thesis: verum

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);

now :: thesis: for i being object st i in I holds
PC . i is non-empty MSAlgebra over S

let i be object ; :: thesis: ( i in I implies PC . i is non-empty MSAlgebra over S )
assume i in I ; :: thesis: PC . i is non-empty MSAlgebra over S
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: verum

end;

then reconsider PC = PC as MSAlgebra-Family of I,S by PRALG_2:def 5;
take PC ; :: thesis: 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 )
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: verum

end;