let D be non empty set ; :: thesis: for n being Element of NAT st D is countable holds
n -tuples_on D is countable
let n be Element of NAT ; :: thesis: ( D is countable implies n -tuples_on D is countable )
assume card D c= omega ; :: according to CARD_3:def 15 :: thesis: n -tuples_on D is countable
then card (1 -tuples_on D) c= omega by Th56;
then A1: 1 -tuples_on D is countable by CARD_3:def 15;
defpred S₁[ Nat] means $1 -tuples_on D is countable;
{(<*> D)} is countable ;
then A2: S₁[ 0 ] by FINSEQ_2:112;
A3: 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 S₁[k] ; :: thesis: S₁[k + 1]
then ( [:(k -tuples_on D),(1 -tuples_on D):] is countable & [:(k -tuples_on D),(1 -tuples_on D):],(k + 1) -tuples_on D are_equipotent ) by A1, Th55, Th57, X;
then ( card [:(k -tuples_on D),(1 -tuples_on D):] c= omega & card [:(k -tuples_on D),(1 -tuples_on D):] = card ((k + 1) -tuples_on D) ) by CARD_3:def 15, CARD_1:21;
hence S₁[k + 1] by CARD_3:def 15; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence n -tuples_on D is countable ; :: thesis: verum