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 rng f is finite by Th26;
then [:(dom f),(rng f):] is finite by A1;
hence f is finite by Th13, RELAT_1:21; :: 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