let D be non empty set ; :: thesis: ( not D is finite implies card D = card (D *) )
defpred S₁[ set ] means verum;
deffunc H₁( Nat) -> FinSequenceSet of D = $1 -tuples_on D;
A1: D * = union { (k -tuples_on D) where k is Nat : verum } by FINSEQ_2:108;
assume A2: not D is finite ; :: thesis: card D = card (D *)
A3: for X being set st X in { (k -tuples_on D) where k is Nat : verum } holds
card X c= card D

proof

let X be set ; :: thesis: ( X in { (k -tuples_on D) where k is Nat : verum } implies card X c= card D )
assume X in { (k -tuples_on D) where k is Nat : verum } ; :: thesis: card X c= card D
then consider k being Nat such that
A4: X = k -tuples_on D ;
0 -tuples_on D = {(<*> D)} by FINSEQ_2:94;
then ( ( card (0 -tuples_on D) c= card D & k = 0 ) or k <> 0 ) by A2;
hence card X c= card D by A2, A4, Th23; :: thesis: verum

end;

1 -tuples_on D in { (k -tuples_on D) where k is Nat : verum } ;
then card (1 -tuples_on D) c= card (D *) by A1, CARD_1:11, ZFMISC_1:74;
then A5: card D c= card (D *) by Th8;
{ H₁(k) where k is Nat : S₁[k] } is countable from CARD_4:sch 1();
then card { (k -tuples_on D) where k is Nat : verum } c= omega ;
then card (union { (k -tuples_on D) where k is Nat : verum } ) c= omega *` (card D) by A3, CARD_2:87;
then card (D *) c= card D by A2, A1, Th21;
hence card D = card (D *) by A5; :: thesis: verum