let D be non empty set ; :: thesis: ( not D is finite implies card D = card (D * ) )
assume A1: not D is finite ; :: thesis: card D = card (D * )
deffunc H₁( Element of NAT ) -> FinSequenceSet of D = $1 -tuples_on D;
defpred S₁[ set ] means verum;
{ H₁(k) where k is Element of NAT : S₁[k] } is countable from CARD_4:sch 1();
then A2: card { (k -tuples_on D) where k is Element of NAT : verum } c= omega by CARD_3:def 15;
for X being set st X in { (k -tuples_on D) where k is Element of NAT : verum } holds
card X c= card D

proof

let X be set ; :: thesis: ( X in { (k -tuples_on D) where k is Element of NAT : verum } implies card X c= card D )
assume X in { (k -tuples_on D) where k is Element of NAT : verum } ; :: thesis: card X c= card D
then consider k being Element of NAT such that
A3: X = k -tuples_on D ;
0 -tuples_on D = {(<*> D)} by FINSEQ_2:112;
then ( ( card (0 -tuples_on D) c= card D & k = 0 ) or k <> 0 ) by A1;
hence card X c= card D by A1, A3, Th86; :: thesis: verum

end;

then A4: card (union { (k -tuples_on D) where k is Element of NAT : verum } ) c= omega *` (card D) by A2, CARD_3:133;
A5: D * = union { (k -tuples_on D) where k is Element of NAT : verum } by FINSEQ_2:128;
then A6: card (D * ) c= card D by A1, A4, Th84;
1 -tuples_on D in { (k -tuples_on D) where k is Element of NAT : verum } ;
then card (1 -tuples_on D) c= card (D * ) by A5, CARD_1:27, ZFMISC_1:92;
then card D c= card (D * ) by Th56;
hence card D = card (D * ) by A6, XBOOLE_0:def 10; :: thesis: verum