deffunc H1( set ) -> set = proj2 $1;
let X be infinite set ; :: thesis: card (Fin X) = card X
set FX = Fin X;
consider f being Function such that
A1: ( dom f = X * & ( for a being set st a in X * holds
f . a = H1(a) ) ) from FUNCT_1:sch 5();
 Fin X c= rng f
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Fin X or a in rng f )
reconsider aa = a as set by TARSKI:1;
assume A2: a in Fin X ; :: thesis: a in rng f
then aa is finite by FINSUB_1:def 5;
then consider p being FinSequence such that
A3: a = rng p by FINSEQ_1:52;
aa c= X by A2, FINSUB_1:def 5;
then p is FinSequence of X by A3, FINSEQ_1:def 4;
then A4: p in X * by FINSEQ_1:def 11;
then f . p in rng f by A1, FUNCT_1:def 3;
hence a in rng f by A1, A3, A4; :: thesis: verum
end;
then card (Fin X) c= card (X *) by A1, CARD_1:12;
hence card (Fin X) c= card X by CARD_4:24; :: according to XBOOLE_0:def 10 :: thesis: card X c= card (Fin X)
set SX = SmallestPartition X;
SmallestPartition X c= Fin X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in SmallestPartition X or a in Fin X )
assume a in SmallestPartition X ; :: thesis: a in Fin X
then a in { {x} where x is Element of X : verum } by EQREL_1:37;
then ex x being Element of X st a = {x} ;
hence a in Fin X by FINSUB_1:def 5; :: thesis: verum
end;
then card (SmallestPartition X) c= card (Fin X) by CARD_1:11;
hence card X c= card (Fin X) by Th12; :: thesis: verum