let a, b be Real; :: thesis: 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 ; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: |.(integral (h,a,b)).| <= integral (|.h.|,a,b)
['a,b'] = [.a,b.] by ;
then A2: integral (h,a,b) = integral (h,['a,b']) by INTEGR15:19;
integral (|.h.|,a,b) = integral (|.h.|,['a,b']) by ;
hence |.(integral (h,a,b)).| <= integral (|.h.|,a,b) by Th20, A1, A2; :: thesis: verum