theorem Th21: :: INTEGR19:21

for a, b being Real
for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds
|.(integral (h,a,b)).| <= integral (|.h.|,a,b)