let i be natural number ; :: 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)
.= Funcs ((Seg i),D) by CARD_3:11
.= i -tuples_on D by FINSEQ_2:93 ; :: thesis: verum