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