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 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; :: thesis: verum