theorem Th23: :: CARD_4:23

for D being non empty set
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 )