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