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