for x being object st x in dom (i |-> D) holds
(i |-> D) . x is finite by FUNCOP_1:7;
then A1: i |-> D is V44() by FINSET_1:def 4;
product (i |-> D) = i -tuples_on D by Th129;
hence i -tuples_on D is finite by A1; :: thesis: verum