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

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