let f be Function; :: thesis: ( dom f is finite implies rng f is finite )
assume dom f is finite ; :: thesis: rng f is finite
then f .: (dom f) is finite ;
hence rng f is finite by RELAT_1:113; :: thesis: verum