let f be Function; :: thesis: ( dom f is finite iff f is finite )
thus ( dom f is finite implies f is finite ) :: thesis: ( f is finite implies dom f is finite )

proof

assume A1: dom f is finite ; :: thesis: f is finite
then A2: rng f is finite by Th8;
f c= [:(dom f),(rng f):] by RELAT_1:7;
hence f is finite by A1, A2; :: thesis: verum

end;

(pr1 ((dom f),(rng f))) .: f = dom f by FUNCT_3:79;
hence ( f is finite implies dom f is finite ) ; :: thesis: verum