let f be PartFunc of REAL,REAL; :: thesis: for b being Real st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
max- f is_-infty_ext_Riemann_integrable_on b
let b be Real; :: thesis: ( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b implies max- f is_-infty_ext_Riemann_integrable_on b )
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on b and
A3: abs f is_-infty_ext_Riemann_integrable_on b ; :: thesis: max- f is_-infty_ext_Riemann_integrable_on b
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 b by A1, A2, INTEGR10:11;
then A6: - f is_-infty_ext_Riemann_integrable_on b 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 b by A1, A3, A5, A6, Th65;
hence max- f is_-infty_ext_Riemann_integrable_on b by INTEGRA4:21; :: thesis: verum