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 & |.(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 & |.(integral (f,A)).| <= integral ((abs f),A) ) )
A1: |.(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 & |.(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 & |.(integral (f,A)).| <= integral ((abs f),A) )
then A3: ( f || A is integrable & (f || A) | A is bounded ) ;
thus ( abs f is_integrable_on A & |.(integral (f,A)).| <= integral ((abs f),A) ) by A3, A2, A1, INTEGRA4:23; :: thesis: verum