let X be non empty set ; :: thesis: for n being non zero Nat st n -tuples_on X is finite holds
X is finite
let n be non zero Nat; :: thesis: ( n -tuples_on X is finite implies X is finite )
assume A1: n -tuples_on X is finite ; :: thesis: X is finite
assume A2: not X is finite ; :: thesis: contradiction
then card X = card (n -tuples_on X) by CARD_4:23;
hence contradiction by A1, A2; :: thesis: verum