let A, B be non empty set ; :: thesis: 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
let N, M be ManySortedSet of [:A,B:]; :: thesis: ( ( for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ) implies M = N )
assume for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ; :: thesis: M = N
then for i, j being object st i in A & j in B holds
N . (i,j) = M . (i,j) ;
hence M = N by Th2; :: thesis: verum