let i be Nat; :: thesis: for D being finite set holds i -tuples_on D is finite
let D be finite set ; :: thesis: i -tuples_on D is finite
A1: i is Element of NAT by ORDINAL1:def 12;

per cases ( not D is empty or D is empty ) ;

suppose A2: not D is empty ; :: thesis: i -tuples_on D is finite

A3: now

let x be set ; :: thesis: ( x in dom (i |-> D) implies (i |-> D) . x is finite )
assume x in dom (i |-> D) ; :: thesis: (i |-> D) . x is finite
then x in Seg i by FUNCOP_1:13;
hence (i |-> D) . x is finite by FUNCOP_1:7; :: thesis: verum

end;

product (i |-> D) = i -tuples_on D by A1, A2, FINSEQ_3:131;
hence i -tuples_on D is finite by A3, MSSCYC_1:1; :: thesis: verum

end;

suppose A4: D is empty ; :: thesis: i -tuples_on D is finite

now

per cases ( i <> 0 or i = 0 ) ;

suppose i <> 0 ; :: thesis: i -tuples_on D is finite

hence i -tuples_on D is finite by A4, FINSEQ_3:119; :: thesis: verum

end;

suppose i = 0 ; :: thesis: i -tuples_on D is finite

then i -tuples_on D = {(<*> D)} by FINSEQ_2:94;
hence i -tuples_on D is finite ; :: thesis: verum

end;

end;

end;

hence i -tuples_on D is finite ; :: thesis: verum

end;

end;