theorem Th1921:
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)