let I be set ; :: thesis: for X being ManySortedSet of I holds X \ ([[0]] I) = X
let X be ManySortedSet of I; :: thesis: X \ ([[0]] I) = X

now

let i be set ; :: thesis: ( i in I implies (X \ ([[0]] I)) . i = X . i )
assume i in I ; :: thesis: (X \ ([[0]] I)) . i = X . i
hence (X \ ([[0]] I)) . i = (X . i) \ (([[0]] I) . i) by Def9
.= (X . i) \ {} by Th5
.= X . i ;
:: thesis: verum

end;

hence X \ ([[0]] I) = X by Th3; :: thesis: verum