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 & is_integrable_on A holds
||.(integral (f,A)).|| <= integral (,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 & is_integrable_on A holds
||.(integral (f,A)).|| <= integral (,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 & is_integrable_on A implies ||.(integral (f,A)).|| <= integral (,A) )
assume A1: ( A c= dom f & f | A is bounded & f is_integrable_on A & is_integrable_on A ) ; :: thesis: ||.(integral (f,A)).|| <= integral (,A)
set g = ;
reconsider fA = f | A as Function of A, the carrier of Y by A1;
A2: integral (f,A) = integral fA by ;
A c= dom by ;
then reconsider gA = | A as Function of A,REAL by Lm3;
A3: gA is integrable by A1;
( fA is bounded & ||.fA.|| = | A ) by ;
hence ||.(integral (f,A)).|| <= integral (,A) by A2, A3, A1, Lm8; :: thesis: verum