defpred S₁[ object , object ] means ex R being RelStr st
( R = C . $1 & $2 = the InternalRel of R );
A1: for i being object st i in I holds
ex j being object st S₁[i,j]

let i be object ; :: thesis:
assume A2: i in I ; :: thesis:
then reconsider I = I as non empty set ;
reconsider B = C as RelStr-yielding ManySortedSet of I ;
reconsider i9 = i as Element of I by A2;
take the InternalRel of (B . i9) ; :: thesis:
take B . i9 ; :: thesis:
thus ( B . i9 = C . i & the InternalRel of (B . i9) = the InternalRel of (B . i9) ) ; :: thesis:

end;

consider M being Function such that
A3: dom M = I and
A4: for i being object st i in I holds
S₁[i,M . i] from CLASSES1:sch 1(A1);
reconsider M = M as ManySortedSet of I by A3, PARTFUN1:def 2, RELAT_1:def 18;
take M ; :: thesis:
thus for i being set st i in I holds
ex P being RelStr st
( P = C . i & M . i = the InternalRel of P ) by A4; :: thesis: