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 | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) holds
( f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) )
let a, b, c be Real; :: thesis: ( a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies ( f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) )
assume that
A1: ( a < b & b <= c ) and
A2: ].a,c.] c= dom f and
A3: f | ['b,c'] is bounded and
A4: f is_left_improper_integrable_on a,b and
A5: f is_integrable_on ['b,c'] and
A6: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ; :: thesis: ( f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) )
consider I being PartFunc of REAL,REAL such that
A7: dom I = ].a,b.] and
A8: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
A9: ( I is_right_convergent_in a or I is_right_divergent_to+infty_in a or I is_right_divergent_to-infty_in a ) by A4;

A10: now :: thesis: not I is_right_divergent_to+infty_in a

assume I is_right_divergent_to+infty_in a ; :: thesis: contradiction
then not f is_left_ext_Riemann_integrable_on a,b by A7, A8, Th35;
hence contradiction by A4, A6, Th34; :: thesis: verum

end;

now :: thesis: not I is_right_divergent_to-infty_in a

assume I is_right_divergent_to-infty_in a ; :: thesis: contradiction
then not f is_left_ext_Riemann_integrable_on a,b by A7, A8, Th35;
hence contradiction by A4, A6, Th34; :: thesis: verum

end;

then f is_left_ext_Riemann_integrable_on a,b by A4, A7, A8, A9, A10, INTEGR10:def 2;
then A11: ( f is_left_ext_Riemann_integrable_on a,c & ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) ) by A1, A2, A3, A5, Th20;
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,x,c) ) & Intf is_right_convergent_in a ) by A11, INTEGR10:def 2;
hence f is_left_improper_integrable_on a,c by A1, A2, A3, A4, A5, Lm11; :: thesis: left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c))
then left_improper_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) by A11, Th34;
hence left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) by A6, XXREAL_3:def 2; :: thesis: verum