defpred S₁[ object , object ] means $2 = (F . $1) .: (A . $1);
A1: for i being object st i in I holds
ex u being object st S₁[i,u] ;
consider g being Function such that
A2: ( dom g = I & ( for i being object st i in I holds
S₁[i,g . i] ) ) from CLASSES1:sch 1(A1);
reconsider g = g as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;
take g ; :: thesis: for i being set st i in I holds
g . i = (F . i) .: (A . i)
thus for i being set st i in I holds
g . i = (F . i) .: (A . i) by A2; :: thesis: verum