let a, b be Real; :: thesis: for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
||.(integral (f,a,b)).|| <= integral (||.f.||,a,b)
let Y be RealBanachSpace; :: thesis: for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
||.(integral (f,a,b)).|| <= integral (||.f.||,a,b)
let f be PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ||.(integral (f,a,b)).|| <= integral (||.f.||,a,b) )
assume A1: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ; :: thesis: ||.(integral (f,a,b)).|| <= integral (||.f.||,a,b)
['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A3: integral (f,a,b) = integral (f,['a,b']) by INTEGR18:16;
integral (||.f.||,a,b) = integral (||.f.||,['a,b']) by A1, INTEGRA5:def 4;
hence ||.(integral (f,a,b)).|| <= integral (||.f.||,a,b) by Th1920, A1, A3; :: thesis: verum