set x = the Element of X;
A1: dom f = X by FUNCT_2:def 1;
thus not f .: X is empty by A1; :: thesis: verum