let A be non empty closed_interval Subset of REAL; :: thesis: for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y st A c= dom f & f | A is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A holds
||.(integral (f,A)).|| <= integral (||.f.||,A)
let Y be RealBanachSpace; :: thesis: for f being PartFunc of REAL, the carrier of Y st A c= dom f & f | A is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A holds
||.(integral (f,A)).|| <= integral (||.f.||,A)
let f be PartFunc of REAL, the carrier of Y; :: thesis: ( A c= dom f & f | A is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A implies ||.(integral (f,A)).|| <= integral (||.f.||,A) )
assume A1: ( A c= dom f & f | A is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A ) ; :: thesis: ||.(integral (f,A)).|| <= integral (||.f.||,A)
set g = ||.f.||;
reconsider fA = f | A as Function of A, the carrier of Y by A1;
A2: integral (f,A) = integral fA by A1, INTEGR18:9;
A c= dom ||.f.|| by A1, NORMSP_0:def 2;
then reconsider gA = ||.f.|| | A as Function of A,REAL by Lm3;
A3: gA is integrable by A1;
( fA is bounded & ||.fA.|| = ||.f.|| | A ) by Th1918, A1;
hence ||.(integral (f,A)).|| <= integral (||.f.||,A) by A2, A3, A1, Lm8; :: thesis: verum