theorem Th3: :: ALTCAT_1:7

for A, B being non empty set
for N, M being ManySortedSet of [:A,B:] st ( for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ) holds
M = N