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 A1, Lm9;
A2: integral (h,A) = integral hA by INTEGR15:14;
A c= dom |.h.| by A1, NFCONT_4:def 2;
then reconsider fA = |.h.| | A as Function of A,REAL by Lm5;
A3: fA is integrable by A1;
A4: hA is integrable by A1, INTEGR15:13;
|.hA.| = |.(h | A).| by Th17
.= |.h.| | A by Th18, A1 ;
hence |.(integral (h,A)).| <= integral (|.h.|,A) by A2, A3, A4, A1, Th16, Lm8; :: thesis: verum