defpred S₁[ object , object ] means ex o1 being Object of C st
( o1 = f . $1 & $2 is Morphism of o1,o );
A1: for i being object st i in I holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume i in I ; :: thesis: ex j being object st S₁[i,j]
then reconsider o1 = f . i as Object of C by FUNCT_2:5;
take the Morphism of o1,o ; :: thesis: S₁[i, the Morphism of o1,o]
thus S₁[i, the Morphism of o1,o] ; :: thesis: verum

end;

ex f being ManySortedSet of I st
for i being object st i in I holds
S₁[i,f . i] from PBOOLE:sch 3(A1);
hence ex b₁ being ManySortedSet of I st
for i being object st i in I holds
ex o1 being Object of C st
( o1 = f . i & b₁ . i is Morphism of o1,o ) ; :: thesis: verum