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

A9: 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,c by A6, A7, Th35;
hence contradiction by A2, A3, Th34; :: thesis: verum

end;

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,c by A6, A7, Th35;
hence contradiction by A2, A3, Th34; :: thesis: verum

end;

reconsider AB = ].a,b.] as non empty Subset of REAL by A4, XXREAL_1:2;
deffunc H₁( Element of AB) -> Element of REAL = In ((integral (f,$1,b)),REAL);
consider Intf being Function of AB,REAL such that
A11: for x being Element of AB holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A12: dom Intf = AB by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b)

proof

let x be Real; :: thesis: ( x in dom Intf implies Intf . x = integral (f,x,b) )
assume x in dom Intf ; :: thesis: Intf . x = integral (f,x,b)
then Intf . x = In ((integral (f,x,b)),REAL) by A11, A12;
hence Intf . x = integral (f,x,b) ; :: thesis: verum

end;

A14: for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom Intf )

proof

let r be Real; :: thesis: ( a < r implies ex g being Real st
( g < r & a < g & g in dom Intf ) )
assume A15: a < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom Intf )
set R = min (b,r);
consider g being Real such that
A16: ( g < min (b,r) & a < g & g in dom I ) by A8, A9, A10, A15, A4, XXREAL_0:21, LIMFUNC2:10;
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
then A17: ( g < b & g < r ) by A16, XXREAL_0:2;
then g in ].a,b.] by A16, XXREAL_1:2;
hence ex g being Real st
( g < r & a < g & g in dom Intf ) by A12, A17, A16; :: thesis: verum

end;

consider g being Real such that
A18: for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom I holds
|.((I . r1) - g).| < g1 ) ) by A8, A9, A10, LIMFUNC2:10;
set G = g - (integral (f,b,c));
A19: for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 ) ) )
assume 0 < g1 ; :: thesis: ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 ) )
then consider r being Real such that
A20: a < r and
A21: for r1 being Real st r1 < r & a < r1 & r1 in dom I holds
|.((I . r1) - g).| < g1 by A18;
set R = min (b,r);
for r1 being Real st r1 < min (b,r) & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1

proof

let r1 be Real; :: thesis: ( r1 < min (b,r) & a < r1 & r1 in dom Intf implies |.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 )
assume that
A22: r1 < min (b,r) and
A23: a < r1 and
A24: r1 in dom Intf ; :: thesis: |.((Intf . r1) - (g - (integral (f,b,c)))).| < g1
( min (b,r) <= r & min (b,r) <= b ) by XXREAL_0:17;
then A25: ( r1 < r & r1 < b ) by A22, XXREAL_0:2;
A26: dom Intf c= dom I by A4, A6, A12, XXREAL_1:42;
then A27: |.((I . r1) - g).| < g1 by A25, A23, A21, A24;
A28: r1 <= c by A6, A24, A26, XXREAL_1:2;
then A29: ( f is_integrable_on ['r1,c'] & f | ['r1,c'] is bounded ) by A2, A23;
A30: [.r1,c.] = ['r1,c'] by A28, INTEGRA5:def 3;
then ['r1,c'] c= ].a,c.] by A23, XXREAL_1:39;
then A31: ['r1,c'] c= dom f by A1;
A32: b in ['r1,c'] by A25, A4, A30, XXREAL_1:1;
(I . r1) - g = (integral (f,r1,c)) - g by A7, A24, A26
.= ((integral (f,r1,b)) + (integral (f,b,c))) - g by A28, A29, A31, A32, INTEGRA6:17
.= (integral (f,r1,b)) - (g - (integral (f,b,c))) ;
hence |.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 by A24, A27, A13; :: thesis: verum

end;

hence ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 ) ) by A20, A4, XXREAL_0:21; :: thesis: verum

end;

hence A33: f is_left_improper_integrable_on a,b by A12, A13, A14, A1, A2, A4, Lm7, LIMFUNC2:10; :: thesis: left_improper_integral (f,a,b) = ext_left_integral (f,a,b)
f is_left_ext_Riemann_integrable_on a,b by A5, A12, A13, A14, A19, LIMFUNC2:10, INTEGR10:def 2;
hence left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A33, Th34; :: thesis: verum