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