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 Th26;
f c= [:(dom f),(rng f):] by RELAT_1:21;
hence f is finite by A1, A2; :: thesis: verum

end;

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