theorem Th2: :: ALTCAT_1:6

for A, B being set
for N, M being ManySortedSet of [:A,B:] st ( for i, j being object st i in A & j in B holds
N . (i,j) = M . (i,j) ) holds
M = N