theorem :: RVSUM_2:53

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