consider x being Element of X;
let f be ManySortedSet of X; :: thesis: not f is empty
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