let i be Nat; :: thesis: for D being set holds product (i |-> D) = i -tuples_on D
let D be 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