let I be non empty set ; :: thesis: for x being ManySortedSet of I holds not x in [[0]] I
consider i being Element of I;
given x being ManySortedSet of I such that A1: x in [[0]] I ; :: thesis: contradiction
x . i in ([[0]] I) . i by A1, Def4;
hence contradiction by FUNCOP_1:13; :: thesis: verum