set x = the Element of X;
A1: dom f = X by FUNCT_2:def 1;
then f . the Element of X in rng f by FUNCT_1:def 3;
hence not f .: X is empty by A1, FUNCT_1:def 6; :: thesis: verum