consider a being Element of A;
( rng f c= H₃(G) & dom f = A ) by Th20;
then f . a in rng f by FUNCT_1:def 5;
hence not rng f is empty ; :: thesis: verum