now :: thesis: for x being object st x in dom (i |-> D) holds
(i |-> D) . x is finite

let x be object ; :: 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;

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