for A being non empty closed_interval Subset of REAL
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)