let I be set ; :: thesis: for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i = Y . i ) holds
X = Y
let X, Y be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds
X . i = Y . i ) implies X = Y )
( dom X = I & dom Y = I ) by PARTFUN1:def 4;
hence ( ( for i being set st i in I holds
X . i = Y . i ) implies X = Y ) by FUNCT_1:9; :: thesis: verum