defpred S₁[ set , set ] means $2 is MSAlgebra-Family of J . $1,S;
A1: for i being set st i in I holds
ex F being set st S₁[i,F]

proof

let i be set ; :: thesis: ( i in I implies ex F being set st S₁[i,F] )
assume i in I ; :: thesis: ex F being set st S₁[i,F]
consider F being MSAlgebra-Family of J . i,S;
take F ; :: thesis: S₁[i,F]
thus S₁[i,F] ; :: thesis: verum

end;

consider C being ManySortedSet of I such that
A2: for i being set 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