let D be non empty set ; :: thesis: for n being Nat st not D is finite & n <> 0 holds
( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D )
let n be Nat; :: thesis: ( not D is finite & n <> 0 implies ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) )
assume that
A1: not D is finite and
A2: n <> 0 ; :: thesis: ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D )
defpred S₁[ Nat] means ( $1 <> 0 implies card ($1 -tuples_on D) = card D );
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
0 -tuples_on D = {(<*> D)} by FINSEQ_2:94;
then A4: ( 0 in card (0 -tuples_on D) & card (0 -tuples_on D) c= card D ) by A1, ORDINAL3:8;
A5: card ((k + 1) -tuples_on D) = card [:(k -tuples_on D),(1 -tuples_on D):] by Th9
.= card [:(card (k -tuples_on D)),(card (1 -tuples_on D)):] by CARD_2:7
.= card [:(card (k -tuples_on D)),(card D):] by Th8
.= (card (k -tuples_on D)) *` (card D) by CARD_2:def 2 ;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A1, A5, A4, Th16; :: thesis: verum

end;

A6: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A3);
then card (n -tuples_on D) = card D by A2;
hence ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) by CARD_1:5; :: thesis: verum