dom f = A by FUNCT_2:def 1;
then f . a in rng f by FUNCT_1:def 3;
hence not f . a is empty ; :: thesis: verum