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