let C, D be non-empty ManySortedSet of the carrier of S; :: thesis: ( ( for s being Element of S holds C . s = Class (R . s) ) & ( for s being Element of S holds D . s = Class (R . s) ) implies C = D )
assume that
A3: for s being Element of S holds C . s = Class (R . s) and
A4: for s being Element of S holds D . s = Class (R . s) ; :: thesis: C = D

now :: thesis: for i being object st i in the carrier of S holds
C . i = D . i

let i be object ; :: thesis: ( i in the carrier of S implies C . i = D . i )
assume i in the carrier of S ; :: thesis: C . i = D . i
then reconsider s = i as Element of S ;
C . s = Class (R . s) by A3;
hence C . i = D . i by A4; :: thesis: verum

end;

hence C = D by PBOOLE:3; :: thesis: verum