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]

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

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: