for r being Real
for f being real-valued FinSequence holds |.(r * f).| = |.r.| * |.f.|