theorem FPA: :: FINSEQ_9:40

for a, b being Complex
for n being Nat
for f, g being b₃ -element complex-valued FinSequence holds (f ^ <*a*>) + (g ^ <*b*>) = (f + g) ^ <*(a + b)*>