let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b holds
max- f is_left_ext_Riemann_integrable_on a,b
let a, b be Real; :: thesis: ( a < b & ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b implies max- f is_left_ext_Riemann_integrable_on a,b )
assume that
A1: a < b and
A2: ].a,b.] c= dom f and
A3: f is_left_ext_Riemann_integrable_on a,b and
A4: abs f is_left_ext_Riemann_integrable_on a,b ; :: thesis: max- f is_left_ext_Riemann_integrable_on a,b
A5: - f = (- 1) (#) f by VALUED_1:def 6;
then A6: dom (- f) = dom f by VALUED_1:def 5;
A7: - f is_left_ext_Riemann_integrable_on a,b by A2, A3, A5, INTEGR24:30;
abs (- f) = |.(- 1).| (#) (abs f) by A5, RFUNCT_1:25
.= (- (- 1)) (#) (abs f) by COMPLEX1:70
.= abs f ;
then max+ (- f) is_left_ext_Riemann_integrable_on a,b by A1, A2, A4, A6, A7, Th63;
hence max- f is_left_ext_Riemann_integrable_on a,b by INTEGRA4:21; :: thesis: verum