let A be non empty 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:46;
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 1;
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 1; :: thesis: verum