defpred S1[ object , object ] means ex j being Element of I * st
( j = $1 & $2 = product (M * j) );
A1: for i being object st i in I * holds
ex j being object st S1[i,j]
proof
let i be object ; :: thesis: ( i in I * implies ex j being object st S1[i,j] )
assume i in I * ; :: thesis: ex j being object st S1[i,j]
then reconsider j = i as Element of I * ;
reconsider e = product (M * j) as set ;
take e ; :: thesis: S1[i,e]
take j ; :: thesis: ( j = i & e = product (M * j) )
thus ( j = i & e = product (M * j) ) ; :: thesis: verum
end;
consider f being ManySortedSet of I * such that
A2: for i being object st i in I * holds
S1[i,f . i] from PBOOLE:sch 3(A1);
 take f ; :: thesis: for i being Element of I * holds f . i = product (M * i)
let i be Element of I * ; :: thesis: f . i = product (M * i)
ex j being Element of I * st
( j = i & f . i = product (M * j) ) by A2;
hence f . i = product (M * i) ; :: thesis: verum