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

let x be object ; :: thesis:
assume A3: x in [:A,B:] ; :: thesis:
then reconsider A1 = A, B1 = B as non empty set ;
consider i being Element of A1, j being Element of B1 such that
A4: x = [i,j] by A3, DOMAIN_1:1;
thus N . x = N . (i,j) by A4
.= M . (i,j) by A1
.= M . x by A4 ; :: thesis:

end;