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

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