let x be Real; :: thesis: for n being Nat
for f being Element of REAL n st 0 <= x & x <= 1 holds
|.(x * f).| <= |.f.|
let n be Nat; :: thesis: for f being Element of REAL n st 0 <= x & x <= 1 holds
|.(x * f).| <= |.f.|
let f be Element of REAL n; :: thesis: ( 0 <= x & x <= 1 implies |.(x * f).| <= |.f.| )
assume that
A1: 0 <= x and
A2: x <= 1 ; :: thesis: |.(x * f).| <= |.f.|
( |.(x * f).| = |.x.| * |.f.| & x = |.x.| ) by A1, ABSVALUE:def 1, EUCLID:11;
then |.(x * f).| <= 1 * |.f.| by A1, A2, XREAL_1:66;
hence |.(x * f).| <= |.f.| ; :: thesis: verum