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:84, CARD_3:102;
then consider f being Function such that
A1: ( f is one-to-one & dom f = NAT & rng f c= X ) by CARD_1:26;

now

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

end;

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