let a, b be real number ; :: thesis: for n being non empty 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 empty 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)
A2: ( a is Real & b is Real ) by XREAL_0:def 1;
['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A3: integral (h,a,b) = integral (h,['a,b']) by A2, 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, A3; :: thesis: verum