let I be set ; :: thesis: for X being ManySortedSet of I holds X (\) (EmptyMS I) = X
let X be ManySortedSet of I; :: thesis: X (\) (EmptyMS I) = X
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( i in I implies (X (\) (EmptyMS I)) . i = X . i )
assume i in I ; :: thesis: (X (\) (EmptyMS I)) . i = X . i
hence (X (\) (EmptyMS I)) . i = (X . i) \ ((EmptyMS I) . i) by Def6
.= (X . i) \ {}
.= X . i ;
:: thesis: verum