let x be real number ; :: thesis: for n being Element of NAT
for f being Element of REAL n st 0 <= x & x <= 1 holds
|.(x * f).| <= |.f.|
let n be Element of 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.|
A3: |.(x * f).| = (abs x) * |.f.| by EUCLID:14;
x = abs x by A1, ABSVALUE:def 1;
then |.(x * f).| <= 1 * |.f.| by A1, A2, A3, XREAL_1:68;
hence |.(x * f).| <= |.f.| ; :: thesis: verum