let f be Function; :: thesis: ( dom f is finite implies f is finite )
assume A1: dom f is finite ; :: thesis: f is finite
then rng f is finite by FINSET_1:8;
then [:(dom f),(rng f):] is finite by A1;
hence f is finite by FINSET_1:1, RELAT_1:7; :: thesis: verum