let I be set ; :: thesis: for X being ManySortedSet of I holds EmptyMS I c= X
let X be ManySortedSet of I; :: thesis: EmptyMS I c= X
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies (EmptyMS I) . i c= X . i )
assume A1: i in I ; :: thesis: (EmptyMS I) . i c= X . i
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (EmptyMS I) . i or e in X . i )
assume e in (EmptyMS I) . i ; :: thesis: e in X . i
hence e in X . i by A1, FUNCOP_1:7; :: thesis: verum