let X be infinite set ; :: thesis: for n being Nat ex Y being finite Subset of X st card Y > n
let n be Nat; :: thesis: ex Y being finite Subset of X st card Y > n
consider f being sequence of X such that
A1: f is one-to-one by DICKSON:3;
set Sn = Seg (n + 1);
reconsider ff = f | (Seg (n + 1)) as Function of (Seg (n + 1)),X by FUNCT_2:32;
ff is one-to-one by A1, FUNCT_1:52;
then card ff = card (rng ff) by PRE_POLY:19;
then A2: card (dom ff) = card (rng ff) by CARD_1:62;
reconsider Y = rng ff as finite Subset of X by RELAT_1:def 19;
take Y ; :: thesis: card Y > n
dom ff = Seg (n + 1) by FUNCT_2:def 1;
then card (dom ff) = n + 1 by FINSEQ_1:57;
hence card Y > n by A2, NAT_1:13; :: thesis: verum