for a being Real
for x being complex-valued FinSequence holds len (a * x) = len x