theorem :: FINSEQ_9:51

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))*>