let i be Nat; :: thesis: for D being non empty set
for x being Element of i -tuples_on D holds dom x = Seg i
let D be non empty set ; :: thesis: for x being Element of i -tuples_on D holds dom x = Seg i
let x be Element of i -tuples_on D; :: thesis: dom x = Seg i
len x = i by Th109;
hence dom x = Seg i by FINSEQ_1:def 3; :: thesis: verum