let X be set ; :: thesis: ( X is countable implies Fin X is countable )
defpred S₁[ object , object ] means ex p being FinSequence st
( $2 = p & $1 = rng p );
A1: ( ( X = {} & {{}} is countable ) or X <> {} ) ;
A2: for a being object st a in Fin X holds
ex b being object st
( b in X * & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in Fin X implies ex b being object st
( b in X * & S₁[a,b] ) )
reconsider aa = a as set by TARSKI:1;
assume A3: a in Fin X ; :: thesis: ex b being object st
( b in X * & S₁[a,b] )
then aa is finite by FINSUB_1:def 5;
then consider p being FinSequence such that
A4: a = rng p by FINSEQ_1:52;
aa 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 object 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 object st a in Fin X holds
S₁[a,f . a] from FUNCT_1:sch 6(A2);
f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom 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 ;
hence card (Fin X) c= omega by A10; :: according to CARD_3:def 14 :: thesis: verum