let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st [.a,b.[ c= dom f & max+ f is_right_ext_Riemann_integrable_on a,b & max- f is_right_ext_Riemann_integrable_on a,b holds
( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) )
let a, b be Real; :: thesis: ( [.a,b.[ c= dom f & max+ f is_right_ext_Riemann_integrable_on a,b & max- f is_right_ext_Riemann_integrable_on a,b implies ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) ) )
assume that
A1: [.a,b.[ c= dom f and
A2: max+ f is_right_ext_Riemann_integrable_on a,b and
A3: max- f is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) )
A4: max+ f is_right_improper_integrable_on a,b by A2, INTEGR24:33;
A5: max- f is_right_improper_integrable_on a,b by A3, INTEGR24:33;
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),a,x) and
A8: I1 is_left_convergent_in b by A2, INTEGR10:def 1;
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),a,x) and
A11: I2 is_left_convergent_in b by A3, INTEGR10:def 1;
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 ['a,d'] & f | ['a,d'] is bounded )

proof

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

end;

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

proof

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

end;

A22: for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom (I1 - I2) ) by A16, A6, A8, LIMFUNC2:7;
hence f is_right_ext_Riemann_integrable_on a,b by A13, A16, A17, A8, A11, LIMFUNC2:46, INTEGR10:def 1; :: thesis: right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b))
A23: ( I1 - I2 is_left_convergent_in b & lim_left ((I1 - I2),b) = (lim_left (I1,b)) - (lim_left (I2,b)) ) by A8, A11, A22, LIMFUNC2:46;
then A24: f is_right_improper_integrable_on a,b by A13, A16, A17, INTEGR10:def 1, INTEGR24:33;
A25: ( lim_left (I1,b) = right_improper_integral ((max+ f),a,b) & lim_left (I2,b) = right_improper_integral ((max- f),a,b) ) by A4, A5, A6, A7, A8, A9, A10, A11, INTEGR24:def 4;
then A26: - (lim_left (I2,b)) = - (right_improper_integral ((max- f),a,b)) by XXREAL_3:def 3;
(right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) = (right_improper_integral ((max+ f),a,b)) + (- (right_improper_integral ((max- f),a,b))) by XXREAL_3:def 4
.= (lim_left (I1,b)) + (- (lim_left (I2,b))) by A25, A26, XXREAL_3:def 2 ;
hence right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) by A24, A16, A17, A23, INTEGR24:def 4; :: thesis: verum