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