let f be Function; :: thesis: ( not dom f is finite & f is one-to-one implies not rng f is finite )
assume A1: ( not dom f is finite & f is one-to-one ) ; :: thesis: not rng f is finite
then dom f, rng f are_equipotent by WELLORD2:def 4;
hence not rng f is finite by A1, Th68; :: thesis: verum