let I be set ; :: thesis: for A being ManySortedSet of I holds [[0]] I c= A
let A be ManySortedSet of I; :: thesis: [[0]] I c= A
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or ([[0]] I) . i c= A . i )
assume i in I ; :: thesis: ([[0]] I) . i c= A . i
([[0]] I) . i = {} by PBOOLE:5;
hence ([[0]] I) . i c= A . i by XBOOLE_1:2; :: thesis: verum