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