let A, B be non empty set ; :: thesis: for N, M being ManySortedSet of 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 ; :: 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 set st i in A & j in B holds
N . i,j = M . i,j ;
hence M = N by Th8; :: thesis: verum