consider x being Element of Z;
A1: dom f = X by FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:def 5;
hence not f .: Z is empty by A1, FUNCT_1:def 12; :: thesis: verum