let I be set ; :: thesis: for X being ManySortedSet of I holds [[0]] I c= X
let X be ManySortedSet of I; :: thesis: [[0]] I c= X
let i be set ; :: according to PBOOLE:def 2 :: 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:7; :: thesis: verum