defpred S1[ object , object ] means $2 is MSAlgebra-Family of J . $1,S;
A1: for i being object st i in I holds
ex F being object st S1[i,F]
proof
let i be object ; :: thesis: ( i in I implies ex F being object st S1[i,F] )
assume i in I ; :: thesis: ex F being object st S1[i,F]
set F = the MSAlgebra-Family of J . i,S;
take the MSAlgebra-Family of J . i,S ; :: thesis: S1[i, the MSAlgebra-Family of J . i,S]
thus S1[i, the MSAlgebra-Family of J . i,S] ; :: thesis: verum
end;
consider C being ManySortedSet of I such that
A2: for i being object st i in I holds
S1[i,C . i] from PBOOLE:sch 3(A1);
 take C ; :: thesis: for i being set st i in I holds
C . i is MSAlgebra-Family of J . i,S
thus for i being set st i in I holds
C . i is MSAlgebra-Family of J . i,S by A2; :: thesis: verum