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

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