theorem Th3: :: EUCLID:6

for r being Real
for f being real-valued FinSequence holds abs (r * f) = |.r.| * (abs f) by RFUNCT_1:25;