let X be set ; :: thesis: ( X is countable implies Fin X is countable )
defpred S₁[ set , set ] means ex p being FinSequence st
( $2 = p & $1 = rng p );
A1: ( ( X = {} & {{}} is countable ) or X <> {} ) by CARD_4:1;
A2: 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 A3: a in Fin X ; :: thesis: ex b being set st
( b in X * & S₁[a,b] )
then a is finite by FINSUB_1:def 5;
then consider p being FinSequence such that
A4: a = rng p by FINSEQ_1:52;
a c= X by A3, FINSUB_1:def 5;
then p is FinSequence of X by A4, 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 A4; :: thesis: verum

end;

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

proof

let a be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not a in proj1 f or not b₁ in proj1 f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A7: a in dom f and
A8: b in dom f ; :: thesis: ( not f . a = f . b or a = b )
A9: S₁[b,f . b] by A8, A5, A6;
S₁[a,f . a] by A7, A5, A6;
hence ( not f . a = f . b or a = b ) by A9; :: thesis: verum

end;

then A10: card (Fin X) c= card (X *) by A5, CARD_1:10;
assume X is countable ; :: thesis: Fin X is countable
then X * is countable by A1, CARD_4:13, FUNCT_7:17;
then card (X *) c= omega by CARD_3:def 14;
hence card (Fin X) c= omega by A10, XBOOLE_1:1; :: according to CARD_3:def 14 :: thesis: verum