let i be Element of NAT ; :: thesis: for D being non empty set holds product (i |-> D) = i -tuples_on D
let D be non empty set ; :: thesis: product (i |-> D) = i -tuples_on D
thus product (i |-> D) = product ((Seg i) --> D) by FINSEQ_2:def 2
.= Funcs (Seg i),D by CARD_3:20
.= i -tuples_on D by FINSEQ_2:111 ; :: thesis: verum