let A, B be set ; :: thesis: 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

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

N . (i,j) = M . (i,j) ) implies M = N )

assume A1: for i, j being object st i in A & j in B holds

N . (i,j) = M . (i,j) ; :: thesis: M = N

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

N . (i,j) = M . (i,j) ) holds

M = N

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

N . (i,j) = M . (i,j) ) implies M = N )

assume A1: for i, j being object st i in A & j in B holds

N . (i,j) = M . (i,j) ; :: thesis: M = N

A2: now :: thesis: for x being object st x in [:A,B:] holds

N . x = M . x

( dom M = [:A,B:] & dom N = [:A,B:] )
by PARTFUN1:def 2;N . x = M . x

let x be object ; :: 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 ;

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: verum

end;assume A3: x in [:A,B:] ; :: thesis: N . x = M . x

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: verum

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