let A, B be set ; :: thesis: for N, M being ManySortedSet of [:A,B:] st ( for i, j being set st i in A & j in B holds
N . i,j = M . i,j ) holds
M = N
let N, M be ManySortedSet of [:A,B:]; :: thesis: ( ( for i, j being set st i in A & j in B holds
N . i,j = M . i,j ) implies M = N )
assume A1: for i, j being set st i in A & j in B holds
N . i,j = M . i,j ; :: thesis: M = N
A2: ( dom M = [:A,B:] & dom N = [:A,B:] ) by PBOOLE:def 3;

now

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

end;

hence M = N by A2, FUNCT_1:9; :: thesis: verum