theorem :: FINSEQ_9:48

for a being Complex
for n being non zero Nat
for f being b₂ -element complex-valued FinSequence holds <*a*> + f = <*(a + (f . 1))*>