let A be non empty closed_interval Subset of REAL; :: thesis: for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds
|.(integral (h,A)).| <= integral (|.h.|,A)

let n be non zero Element of NAT ; :: thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds
|.(integral (h,A)).| <= integral (|.h.|,A)

let h be PartFunc of REAL,(REAL n); :: thesis: ( A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A implies |.(integral (h,A)).| <= integral (|.h.|,A) )
assume A1: ( A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A ) ; :: thesis: |.(integral (h,A)).| <= integral (|.h.|,A)
set f = |.h.|;
reconsider hA = h | A as Function of A,(REAL n) by ;
A2: integral (h,A) = integral hA by INTEGR15:14;
A c= dom |.h.| by ;
then reconsider fA = |.h.| | A as Function of A,REAL by Lm5;
A3: fA is integrable by A1;
A4: hA is integrable by ;
|.hA.| = |.(h | A).| by Th17
.= |.h.| | A by ;
hence |.(integral (h,A)).| <= integral (|.h.|,A) by A2, A3, A4, A1, Th16, Lm8; :: thesis: verum