let f be PartFunc of REAL,REAL; :: thesis: for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
max- f is_+infty_ext_Riemann_integrable_on a
let a be Real; :: thesis: ( right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a implies max- f is_+infty_ext_Riemann_integrable_on a )
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a and
A3: abs f is_+infty_ext_Riemann_integrable_on a ; :: thesis: max- f is_+infty_ext_Riemann_integrable_on a
A4: - f = (- 1) (#) f by VALUED_1:def 6;
then A5: dom (- f) = dom f by VALUED_1:def 5;
(- 1) (#) f is_+infty_ext_Riemann_integrable_on a by A1, A2, INTEGR10:9;
then A6: - f is_+infty_ext_Riemann_integrable_on a by VALUED_1:def 6;
abs (- f) = |.(- 1).| (#) (abs f) by A4, RFUNCT_1:25
.= (- (- 1)) (#) (abs f) by COMPLEX1:70
.= abs f ;
then max+ (- f) is_+infty_ext_Riemann_integrable_on a by A1, A3, A5, A6, Th66;
hence max- f is_+infty_ext_Riemann_integrable_on a by INTEGRA4:21; :: thesis: verum