for x being Real
for n being Nat
for f being Element of REAL n st 0 <= x & x <= 1 holds
|.(x * f).| <= |.f.|