let f be PartFunc of REAL,REAL; :: thesis: for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) holds
( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) )
let a, b, c be Real; :: thesis: ( a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies ( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) )
assume that
A1: ( a <= b & b < c ) and
A2: [.a,c.[ c= dom f and
A3: f | ['a,b'] is bounded and
A4: f is_right_improper_integrable_on b,c and
A5: f is_integrable_on ['a,b'] and
A6: right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ; :: thesis: ( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) )
consider I being PartFunc of REAL,REAL such that
A7: dom I = [.b,c.[ and
A8: for x being Real st x in dom I holds
I . x = integral (f,b,x) and
A9: ( I is_left_convergent_in c or I is_left_divergent_to+infty_in c or I is_left_divergent_to-infty_in c ) by A4;

A10: now :: thesis: not I is_left_divergent_to+infty_in c

assume I is_left_divergent_to+infty_in c ; :: thesis: contradiction
then not f is_right_ext_Riemann_integrable_on b,c by A7, A8, Th40;
hence contradiction by A4, A6, Th39; :: thesis: verum

end;

now :: thesis: not I is_left_divergent_to-infty_in c

assume I is_left_divergent_to-infty_in c ; :: thesis: contradiction
then not f is_right_ext_Riemann_integrable_on b,c by A7, A8, Th40;
hence contradiction by A4, A6, Th39; :: thesis: verum

end;

then f is_right_ext_Riemann_integrable_on b,c by A4, A7, A8, A9, A10, INTEGR10:def 1;
then A11: ( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (ext_right_integral (f,b,c)) + (integral (f,a,b)) ) by A1, A2, A3, A5, Th21;
ex Intf being PartFunc of REAL,REAL st
( dom Intf = [.a,c.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in c ) by A11, INTEGR10:def 1;
hence f is_right_improper_integrable_on a,c by A1, A2, A3, A4, A5, Lm19; :: thesis: right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b))
then right_improper_integral (f,a,c) = (ext_right_integral (f,b,c)) + (integral (f,a,b)) by A11, Th39;
hence right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) by A6, XXREAL_3:def 2; :: thesis: verum