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