let a, b be 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)
let n be 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)
let h be PartFunc of REAL,(REAL n); ( a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded implies |.(integral (h,a,b)).| <= integral (|.h.|,a,b) )
assume A1:
( a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded )
; |.(integral (h,a,b)).| <= integral (|.h.|,a,b)
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
then A2:
integral (h,a,b) = integral (h,['a,b'])
by INTEGR15:19;
integral (|.h.|,a,b) = integral (|.h.|,['a,b'])
by A1, INTEGRA5:def 4;
hence
|.(integral (h,a,b)).| <= integral (|.h.|,a,b)
by Th20, A1, A2; verum