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