let X be set ; :: thesis: ( X is countable implies Fin X is countable )
assume A1: X is countable ; :: thesis: Fin X is countable
( ( X = {} & {{} } is countable ) or X <> {} ) by CARD_4:43;
then X * is countable by A1, CARD_4:65, FUNCT_7:19;
then A2: card (X * ) c= omega by CARD_3:def 15;
defpred S₁[ set , set ] means ex p being FinSequence st
( $2 = p & $1 = rng p );
A3: for a being set st a in Fin X holds
ex b being set st
( b in X * & S₁[a,b] )

proof

let a be set ; :: thesis: ( a in Fin X implies ex b being set st
( b in X * & S₁[a,b] ) )
assume a in Fin X ; :: thesis: ex b being set st
( b in X * & S₁[a,b] )
then A4: ( a c= X & a is finite ) by FINSUB_1:def 5;
then consider p being FinSequence such that
A5: a = rng p by FINSEQ_1:73;
p is FinSequence of X by A4, A5, FINSEQ_1:def 4;
then p in X * by FINSEQ_1:def 11;
hence ex b being set st
( b in X * & S₁[a,b] ) by A5; :: thesis: verum

end;

consider f being Function such that
A6: ( dom f = Fin X & rng f c= X * ) and
A7: for a being set st a in Fin X holds
S₁[a,f . a] from WELLORD2:sch 1(A3);
f is one-to-one

proof

let a be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not a in dom f or not b₁ in dom f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume ( a in dom f & b in dom f ) ; :: thesis: ( not f . a = f . b or a = b )
then ( S₁[a,f . a] & S₁[b,f . b] ) by A6, A7;
hence ( not f . a = f . b or a = b ) ; :: thesis: verum

end;

then card (Fin X) c= card (X * ) by A6, CARD_1:26;
hence card (Fin X) c= omega by A2, XBOOLE_1:1; :: according to CARD_3:def 15 :: thesis: verum