let i be Nat; :: thesis: for D being non empty set
for z being Tuple of i,D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
let D be non empty set ; :: thesis: for z being Tuple of i,D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
let z be Tuple of i,D; :: thesis: for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
let d be Element of D; :: thesis: (z ^ <*d*>) . (i + 1) = d
len z = i by FINSEQ_1:def 18;
hence (z ^ <*d*>) . (i + 1) = d by FINSEQ_1:59; :: thesis: verum