for a being Complex
for f being complex-valued FinSequence holds ((len f) |-> a) (#) f = a (#) f