theorem :: TOPALG_1:11

for n being Nat
for f being Element of REAL n
for p being Point of I[01] holds |.(p * f).| <= |.f.|