theorem :: FINSEQ_9:49

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