theorem Th4: :: ALTCAT_1:8

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