theorem :: FINSEQ_9:50

for a being Complex
for n being non zero Nat
for f being b₂ -element complex-valued FinSequence holds <*a*> (#) f = <*(a * (f . 1))*>