set x = the Element of X;
let f be ManySortedSet of X; :: thesis: not f is empty
dom f = X by PARTFUN1:def 2;
then [ the Element of X,(f . the Element of X)] in f by FUNCT_1:def 2;
hence not f is empty ; :: thesis: verum