let i be Nat; :: thesis: for D being non empty set
for x being Tuple of i,D holds dom x = Seg i
let D be non empty set ; :: 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 FINSEQ_1:def 18;
hence dom x = Seg i by FINSEQ_1:def 3; :: thesis: verum