theorem Th1921: :: INTEGR21:21

for a, b being Real
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)