theorem :: FINSEQ_3:103

for i being Nat
for df being FinSequence
for d being object st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i