let n be Nat; :: thesis: for f being Element of REAL n
for p being Point of I[01] holds |.(p * f).| <= |.f.|
let f be Element of REAL n; :: thesis: for p being Point of I[01] holds |.(p * f).| <= |.f.|
let p be Point of I[01]; :: thesis: |.(p * f).| <= |.f.|
( [.0,1.] = { r where r is Real : ( 0 <= r & r <= 1 ) } & p in the carrier of I[01] ) by RCOMP_1:def 1;
then ex r being Real st
( r = p & 0 <= r & r <= 1 ) by BORSUK_1:40;
hence |.(p * f).| <= |.f.| by Th10; :: thesis: verum