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 and
A2: dom f = NAT and
A3: rng f c= X by CARD_1:26;

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:12;
hence f . x in X by A3; :: thesis: verum

end;

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