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;
hence rng f is infinite by A1, Th37; :: thesis: verum