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 ) )
A1: abs (f || A) = (abs f) || A by RFUNCT_1:62;
assume 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 ) )
then A2: f || A is Function of A,REAL by Lm1;
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 A3: ( f || A is integrable & (f || A) | A is bounded ) by INTEGRA5:9, INTEGRA5:def 2;
then abs (f || A) is integrable by A2, INTEGRA4:23;
hence ( abs f is_integrable_on A & abs (integral f,A) <= integral (abs f),A ) by A3, A2, A1, INTEGRA4:23, INTEGRA5:def 2; :: thesis: verum