let D be non empty set ; :: thesis: for i being natural Number
for x being Tuple of i,D holds dom x = Seg i
let i be natural Number ; :: thesis: for x being Tuple of i,D holds dom x = Seg i
let x be Tuple of i,D; :: thesis: dom x = Seg i
len x = i by CARD_1:def 7;
hence dom x = Seg i by FINSEQ_1:def 3; :: thesis: verum