defpred S₁[ object , object ] means ex R being 1-sorted st
( R = A . $1 & $2 = the carrier of R );
A1: for i being object st i in J holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in J implies ex j being object st S₁[i,j] )
assume A2: i in J ; :: thesis: ex j being object st S₁[i,j]
then reconsider J = J as non empty set ;
reconsider i9 = i as Element of J by A2;
reconsider B = A as 1-sorted-yielding ManySortedSet of J ;
take the carrier of (B . i9) ; :: thesis: S₁[i, the carrier of (B . i9)]
take B . i9 ; :: thesis: ( B . i9 = A . i & the carrier of (B . i9) = the carrier of (B . i9) )
thus ( B . i9 = A . i & the carrier of (B . i9) = the carrier of (B . i9) ) ; :: thesis: verum

end;

consider M being Function such that
A3: dom M = J and
A4: for i being object st i in J holds
S₁[i,M . i] from CLASSES1:sch 1(A1);
reconsider M = M as ManySortedSet of J by A3, PARTFUN1:def 2, RELAT_1:def 18;
take M ; :: thesis: for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & M . j = the carrier of R )
thus for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & M . j = the carrier of R ) by A4; :: thesis: verum