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