let I be set ; :: thesis: for x, y being ManySortedSet of st {x} \ {y} = [0] I holds
x = y
let x, y be ManySortedSet of ; :: thesis: ( {x} \ {y} = [0] I implies x = y )
assume A1: {x} \ {y} = [0] I ; :: thesis: x = y

now

let i be set ; :: thesis: ( i in I implies x . i = y . i )
assume A2: i in I ; :: thesis: x . i = y . i
then {(x . i)} \ {(y . i)} = ({x} . i) \ {(y . i)} by Def1
.= ({x} . i) \ ({y} . i) by A2, Def1
.= ({x} \ {y}) . i by A2, PBOOLE:def 9
.= {} by A1, PBOOLE:5 ;
hence x . i = y . i by ZFMISC_1:21; :: thesis: verum

end;

hence x = y by PBOOLE:3; :: thesis: verum