consider a being Element of A;
dom f = A by Th20;
then f . a in rng f by FUNCT_1:def 5;
hence not rng f is empty ; :: thesis: verum