let i be natural Number ; :: 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 CARD_1:def 7;
hence (z ^ <*d*>) . (i + 1) = d by FINSEQ_1:42; :: thesis: verum