let X be infinite set ; :: thesis: ex f being sequence of X st f is one-to-one
card NAT c= card X by 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;
for x being object st x in NAT holds
f . x in X by A3, A2, FUNCT_1:3;
then reconsider f = f as sequence of X by A2, FUNCT_2:3;
take f ; :: thesis: f is one-to-one
thus f is one-to-one by A1; :: thesis: verum