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 K10(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 3();
{ (F ` ) where F is Subset of X : F is finite } c= rng f

proof

let a be set ; :: 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 ` & F is finite ) ;
consider p being FinSequence such that
A3: F = rng p by A2, FINSEQ_1:73;
p is FinSequence of X by A3, FINSEQ_1:def 4;
then p in X * by FINSEQ_1:def 11;
then ( f . p in rng f & f . p = X \ (proj2 p) & proj2 p = F ) by A1, A3, FUNCT_1:def 5;
hence a in rng f by A2; :: thesis: verum

end;

then card { (F ` ) where F is Subset of X : F is finite } c= card (X * ) by A1, CARD_1:28;
hence card { (F ` ) where F is Subset of X : F is finite } c= card X by CARD_4:87; :: according to XBOOLE_0:def 10 :: thesis: card X c= card { (F ` ) where F is Subset of X : F is finite }
deffunc H₂( set ) -> Element of K10(X) = X \ {$1};
consider f being Function such that
A4: ( dom f = X & ( for a being set st a in X holds
f . a = H₂(a) ) ) from FUNCT_1:sch 3();
A5: 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 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 A6: ( a in dom f & b in dom f & f . a = f . b ) ; :: thesis: a = b
then reconsider a = a, b = b as Element of X by A4;
{a} ` = f . b by A4, A6
.= {b} ` by A4 ;
then {a} = {b} by SUBSET_1:64;
hence a = b by ZFMISC_1:6; :: thesis: verum

end;

rng f c= { (F ` ) where F is Subset of X : F is finite }

proof

let a be set ; :: 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 set such that
A7: ( b in dom f & a = f . b ) by FUNCT_1:def 5;
reconsider b = b as Element of X by A4, A7;
( {b} ` in { (F ` ) where F is Subset of X : F is finite } & a = X \ {b} ) by A4, A7;
hence a in { (F ` ) where F is Subset of X : F is finite } ; :: thesis: verum

end;

hence card X c= card { (F ` ) where F is Subset of X : F is finite } by A4, A5, CARD_1:26; :: thesis: verum