theorem FINSEQ940A: :: NEWTON07:52

for a1, a2, b1, b2 being Complex
for n being Nat
for f, g being b₅ -element complex-valued FinSequence holds (f ^ <*a1,a2*>) + (g ^ <*b1,b2*>) = (f + g) ^ <*(a1 + b1),(a2 + b2)*>