let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds
( abs f is_integrable_on A & abs (integral f,A) <= integral (abs f),A )
let f be PartFunc of REAL ,REAL ; :: thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( abs f is_integrable_on A & abs (integral f,A) <= integral (abs f),A ) )
assume A1: A c= dom f ; :: thesis: ( not f is_integrable_on A or not f | A is bounded or ( abs f is_integrable_on A & abs (integral f,A) <= integral (abs f),A ) )
assume ( f is_integrable_on A & f | A is bounded ) ; :: thesis: ( abs f is_integrable_on A & abs (integral f,A) <= integral (abs f),A )
then A2: ( f || A is integrable & (f || A) | A is bounded ) by INTEGRA5:9, INTEGRA5:def 2;
f || A is Function of A,REAL by A1, Lm1;
then A3: ( abs (f || A) is integrable & abs (integral (f || A)) <= integral (abs (f || A)) ) by A2, INTEGRA4:23;
abs (f || A) = (abs f) || A by RFUNCT_1:62;
hence ( abs f is_integrable_on A & abs (integral f,A) <= integral (abs f),A ) by A3, INTEGRA5:def 2; :: thesis: verum