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

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