let f be Function; :: thesis: ( dom f is infinite & f is one-to-one implies rng f is infinite )
assume A1: dom f is infinite ; :: thesis: ( not f is one-to-one or rng f is infinite )
assume f is one-to-one ; :: thesis: rng f is infinite
then dom f, rng f are_equipotent ;
hence rng f is infinite by A1, Th37; :: thesis: verum