theorem FMA: :: FINSEQ_9:44

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