let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st ].a,b.] c= dom f & max+ f is_left_ext_Riemann_integrable_on a,b & max- f is_left_ext_Riemann_integrable_on a,b holds
( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b)) )
let a, b be Real; :: thesis: ( ].a,b.] c= dom f & max+ f is_left_ext_Riemann_integrable_on a,b & max- f is_left_ext_Riemann_integrable_on a,b implies ( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b)) ) )
assume that
A1: ].a,b.] c= dom f and
A2: max+ f is_left_ext_Riemann_integrable_on a,b and
A3: max- f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b)) )
A4: max+ f is_left_improper_integrable_on a,b by A2, INTEGR24:32;
A5: max- f is_left_improper_integrable_on a,b by A3, INTEGR24:32;
consider I1 being PartFunc of REAL,REAL such that
A6: dom I1 = ].a,b.] and
A7: for x being Real st x in dom I1 holds
I1 . x = integral ((max+ f),x,b) and
A8: I1 is_right_convergent_in a by A2, INTEGR10:def 2;
consider I2 being PartFunc of REAL,REAL such that
A9: dom I2 = ].a,b.] and
A10: for x being Real st x in dom I2 holds
I2 . x = integral ((max- f),x,b) and
A11: I2 is_right_convergent_in a by A3, INTEGR10:def 2;
A12: f = (max+ f) - (max- f) by RFUNCT_3:34;
A13: for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )

proof

let d be Real; :: thesis: ( a < d & d <= b implies ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) )
assume A14: ( a < d & d <= b ) ; :: thesis: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
then A15: ( max+ f is_integrable_on ['d,b'] & (max+ f) | ['d,b'] is bounded ) by A2, INTEGR10:def 2;
A16: ( max- f is_integrable_on ['d,b'] & (max- f) | ['d,b'] is bounded ) by A14, A3, INTEGR10:def 2;
['d,b'] = [.d,b.] by A14, INTEGRA5:def 3;
then ['d,b'] c= ].a,b.] by A14, XXREAL_1:39;
then ['d,b'] c= dom f by A1;
then ( ['d,b'] c= dom (max+ f) & ['d,b'] c= dom (max- f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
hence f is_integrable_on ['d,b'] by A12, A15, A16, INTEGRA6:11; :: thesis: f | ['d,b'] is bounded
f | (['d,b'] /\ ['d,b']) is bounded by A12, A15, A16, RFUNCT_1:84;
hence f | ['d,b'] is bounded ; :: thesis: verum

end;

A17: dom (I1 - I2) = ].a,b.] /\ ].a,b.] by A6, A9, VALUED_1:12;
A18: for x being Real st x in dom (I1 - I2) holds
(I1 - I2) . x = integral (f,x,b)

proof

let x be Real; :: thesis: ( x in dom (I1 - I2) implies (I1 - I2) . x = integral (f,x,b) )
assume A19: x in dom (I1 - I2) ; :: thesis: (I1 - I2) . x = integral (f,x,b)
then (I1 - I2) . x = (I1 . x) - (I2 . x) by VALUED_1:13;
then (I1 - I2) . x = (integral ((max+ f),x,b)) - (I2 . x) by A19, A6, A7, A17;
then A20: (I1 - I2) . x = (integral ((max+ f),x,b)) - (integral ((max- f),x,b)) by A19, A9, A10, A17;
A21: ( a < x & x <= b ) by A19, A17, XXREAL_1:2;
then ['x,b'] = [.x,b.] by INTEGRA5:def 3;
then ['x,b'] c= ].a,b.] by A21, XXREAL_1:39;
then ['x,b'] c= dom f by A1;
then A22: ( ['x,b'] c= dom (max+ f) & ['x,b'] c= dom (max- f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
( max+ f is_integrable_on ['x,b'] & (max+ f) | ['x,b'] is bounded & max- f is_integrable_on ['x,b'] & (max- f) | ['x,b'] is bounded ) by A21, A2, A3, INTEGR10:def 2;
hence (I1 - I2) . x = integral (f,x,b) by A20, A21, A22, A12, INTEGRA6:12; :: thesis: verum

end;

A23: for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom (I1 - I2) ) by A17, A6, A8, LIMFUNC2:10;
hence f is_left_ext_Riemann_integrable_on a,b by A13, A17, A18, A8, A11, LIMFUNC2:55, INTEGR10:def 2; :: thesis: left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b))
A24: ( I1 - I2 is_right_convergent_in a & lim_right ((I1 - I2),a) = (lim_right (I1,a)) - (lim_right (I2,a)) ) by A8, A23, A11, LIMFUNC2:55;
then A25: f is_left_improper_integrable_on a,b by A13, A17, A18, INTEGR10:def 2, INTEGR24:32;
A26: ( lim_right (I1,a) = left_improper_integral ((max+ f),a,b) & lim_right (I2,a) = left_improper_integral ((max- f),a,b) ) by A4, A5, A6, A7, A8, A9, A10, A11, INTEGR24:def 3;
then A27: - (lim_right (I2,a)) = - (left_improper_integral ((max- f),a,b)) by XXREAL_3:def 3;
(left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b)) = (left_improper_integral ((max+ f),a,b)) + (- (left_improper_integral ((max- f),a,b))) by XXREAL_3:def 4
.= (lim_right (I1,a)) + (- (lim_right (I2,a))) by A26, A27, XXREAL_3:def 2 ;
hence left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b)) by A25, A17, A18, A24, INTEGR24:def 3; :: thesis: verum