theorem FINSEQ940B: :: NEWTON07:53

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