theorem Th117: :: RVSUM_1:117

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