theorem Th58: :: RVSUM_1:58

for r being Real
for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F)