defpred S₁[ 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 S₁[i,F]

proof

let i be object ; :: thesis: ( i in I implies ex F being object st S₁[i,F] )
assume i in I ; :: thesis: ex F being object st S₁[i,F]
set F = the MSAlgebra-Family of J . i,S;
take the MSAlgebra-Family of J . i,S ; :: thesis: S₁[i, the MSAlgebra-Family of J . i,S]
thus S₁[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
S₁[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