let X be infinite set ; :: thesis: card { (F `) where F is Subset of X : F is finite } = card X
set FX = { (F `) where F is Subset of X : F is finite } ;
deffunc H₁( set ) -> Element of K32(X) = X \ (proj2 $1);
consider f being Function such that
A1: ( dom f = X * & ( for a being set st a in X * holds
f . a = H₁(a) ) ) from FUNCT_1:sch 5();
{ (F `) where F is Subset of X : F is finite } c= rng f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in rng f )
assume a in { (F `) where F is Subset of X : F is finite } ; :: thesis: a in rng f
then consider F being Subset of X such that
A2: a = F ` and
A3: F is finite ;
consider p being FinSequence such that
A4: F = rng p by A3, FINSEQ_1:52;
p is FinSequence of X by A4, FINSEQ_1:def 4;
then A5: 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, A2, A4, A5; :: thesis: verum

end;

then card { (F `) where F is Subset of X : F is finite } c= card (X *) by A1, CARD_1:12;
hence card { (F `) where F is Subset of X : F is finite } c= card X by CARD_4:24; :: according to XBOOLE_0:def 10 :: thesis: card X c= card { (F `) where F is Subset of X : F is finite }
deffunc H<sub>2</sub>( set ) -> Element of K32(X) = X \ {$1};
consider f being Function such that
A6: ( dom f = X & ( for a being set st a in X holds
f . a = H<sub>2</sub>(a) ) ) from FUNCT_1:sch 5();
A7: rng f c= { (F `) where F is Subset of X : F is finite }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in { (F `) where F is Subset of X : F is finite } )
assume a in rng f ; :: thesis: a in { (F `) where F is Subset of X : F is finite }
then consider b being object such that
A8: b in dom f and
A9: a = f . b by FUNCT_1:def 3;
reconsider b = b as Element of X by A6, A8;
{b} ` in { (F `) where F is Subset of X : F is finite } ;
hence a in { (F `) where F is Subset of X : F is finite } by A6, A9; :: thesis: verum

end;

f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A10: a in dom f and
A11: b in dom f and
A12: f . a = f . b ; :: thesis: a = b
reconsider a = a, b = b as Element of X by A6, A10, A11;
{a} ` = f . b by A6, A12
.= {b} ` by A6 ;
then {a} = {b} by SUBSET_1:42;
hence a = b by ZFMISC_1:3; :: thesis: verum

end;

hence card X c= card { (F `) where F is Subset of X : F is finite } by A6, A7, CARD_1:10; :: thesis: verum