let D be non empty set ; :: thesis: for n being Element of 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 Element of NAT ; :: thesis: ( not D is finite & n <> 0 implies ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) )
assume A1: ( not D is finite & 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: S₁[ 0 ] ;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
X: k in NAT by ORDINAL1:def 13;
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
A6: card ((k + 1) -tuples_on D) = card [:(k -tuples_on D),(1 -tuples_on D):] by Th57, X
.= card [:(card (k -tuples_on D)),(card (1 -tuples_on D)):] by CARD_2:14
.= card [:(card (k -tuples_on D)),(card D):] by Th56
.= (card (k -tuples_on D)) *` (card D) by CARD_2:def 2 ;
A7: 0 -tuples_on D = {(<*> D)} by FINSEQ_2:112;
( 0 in card (0 -tuples_on D) & card (0 -tuples_on D) c= card D ) by A1, A7, ORDINAL3:10;
hence S₁[k + 1] by A1, A5, A6, Th78; :: thesis: verum

end;

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