dom f = the carrier of L by FUNCT_2:def 1;
then ( not rng f is empty & rng f = the carrier of (Image f) ) by RELAT_1:65, YELLOW_0:def 15;
hence not Image f is empty ; :: thesis: verum