let n be Nat; :: thesis: for D being non empty set
for d being Element of D
for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d
let D be non empty set ; :: thesis: for d being Element of D
for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d
let d be Element of D; :: thesis: for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d
let z be Tuple of n,D; :: thesis: (z ^ <*d*>) /. (n + 1) = d
len <*d*> = 1 by FINSEQ_1:39;
then 0 + 1 in Seg (len <*d*>) ;
then A1: 0 + 1 in dom <*d*> by FINSEQ_1:def 3;
len z = n by CARD_1:def 7;
hence (z ^ <*d*>) /. (n + 1) = <*d*> /. 1 by A1, FINSEQ_4:69
.= d by FINSEQ_4:16 ;
:: thesis: verum