let X be infinite set ; :: thesis: ex f being Function of NAT,X st f is one-to-one
card NAT c= card X by CARD_1:47, CARD_3:85;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = NAT and
A3: rng f c= X by CARD_1:10;

now

let x be set ; :: thesis: ( x in NAT implies f . x in X )
assume x in NAT ; :: thesis: f . x in X
then f . x in rng f by A2, FUNCT_1:3;
hence f . x in X by A3; :: thesis: verum

end;

then reconsider f = f as Function of NAT,X by A2, FUNCT_2:3;
take f ; :: thesis: f is one-to-one
thus f is one-to-one by A1; :: thesis: verum