theorem Th1: :: BINARITH:1

for i, n being Nat
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