let n be Element of 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.|
A1: [.0 ,1.] = { r where r is Real : ( 0 <= r & r <= 1 ) } by RCOMP_1:def 1;
p in the carrier of I[01] ;
then ex r being Real st
( r = p & 0 <= r & r <= 1 ) by A1, BORSUK_1:83;
hence |.(p * f).| <= |.f.| by Th10; :: thesis: verum