let n be Nat; :: thesis: for X being set holds product ((Seg n) --> X) = n -tuples_on X
let X be set ; :: thesis: product ((Seg n) --> X) = n -tuples_on X
n -tuples_on X = Funcs ((Seg n),X) by FINSEQ_2:93;
hence product ((Seg n) --> X) = n -tuples_on X by CARD_3:11; :: thesis: verum