let f be Function; :: thesis: ( dom f is finite implies f is finite )
assume A1: dom f is finite ; :: thesis: f is finite
A2: rng f is finite by A1, FINSET_1:26;
A3: [:(dom f),(rng f):] is finite by A1, A2;
thus f is finite by A3, FINSET_1:13, RELAT_1:21; :: thesis: verum