let f be PartFunc of REAL,REAL; :: thesis:
let a, b, c be Real; :: thesis:
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) = +infty ; :: thesis:
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;
left_improper_integral (f,a,b) <> ext_left_integral (f,a,b) by A6;
then A10: not f is_left_ext_Riemann_integrable_on a,b by A4, Th34;
reconsider AC = ].a,c.] as non empty Subset of REAL by A1, XXREAL_1:2;
deffunc H₁( Element of AC) -> Element of REAL = In ((integral (f,$1,c)),REAL);
consider Intf being Function of AC,REAL such that
A11: for x being Element of AC holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A12: dom Intf = AC 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,c)

proof

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

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:
assume a < r ; :: thesis:
then consider g being Real such that
A15: ( g < r & a < g & g in dom I ) by A10, A6, A7, Def3, INTEGR10:def 2, A4, LIMFUNC2:11;
].a,b.] c= ].a,c.] by A1, XXREAL_1:42;
hence ex g being Real st
( g < r & a < g & g in dom Intf ) by A15, A7, A12; :: thesis:

end;

A16: for g1 being Real ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
g1 < Intf . r1 ) )

proof

let g1 be Real; :: thesis:
consider r being Real such that
A17: a < r and
A18: for r1 being Real st r1 < r & a < r1 & r1 in dom I holds
g1 - (integral (f,b,c)) < I . r1 by A10, A9, A4, A6, A7, A8, Def3, INTEGR10:def 2, LIMFUNC2:11;
set R = min (b,r);
take min (b,r) ; :: thesis:
thus a < min (b,r) by A1, A17, XXREAL_0:21; :: thesis:
thus for r1 being Real st r1 < min (b,r) & a < r1 & r1 in dom Intf holds
g1 < Intf . r1 :: thesis:

proof

let r1 be Real; :: thesis:
assume A19: ( r1 < min (b,r) & a < r1 & r1 in dom Intf ) ; :: thesis:
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
then A20: ( r1 < b & r1 < r ) by A19, XXREAL_0:2;
then A21: r1 < c by A1, XXREAL_0:2;
r1 in dom I by A7, A19, A20, XXREAL_1:2;
then g1 - (integral (f,b,c)) < I . r1 by A18, A19, A20;
then A22: g1 - (integral (f,b,c)) < integral (f,r1,b) by A8, A20, A7, A19, XXREAL_1:2;
A23: ( f is_integrable_on ['r1,c'] & f | ['r1,c'] is bounded ) by A19, A21, A1, A2, A3, A4, A5, Lm11;
A24: ['r1,c'] = [.r1,c.] by A20, A1, XXREAL_0:2, INTEGRA5:def 3;
then ['r1,c'] c= ].a,c.] by A19, XXREAL_1:39;
then A25: ['r1,c'] c= dom f by A2;
b in ['r1,c'] by A24, A20, A1, XXREAL_1:1;
then integral (f,r1,c) = (integral (f,r1,b)) + (integral (f,b,c)) by A21, A23, A25, INTEGRA6:17;
then integral (f,r1,b) = (integral (f,r1,c)) - (integral (f,b,c)) ;
then g1 < integral (f,r1,c) by A22, XREAL_1:9;
hence g1 < Intf . r1 by A13, A19; :: thesis:

end;

end;

hence A26: f is_left_improper_integrable_on a,c by A12, A13, A14, A1, A2, A3, A4, A5, Lm11, LIMFUNC2:11; :: thesis:
Intf is_right_divergent_to+infty_in a by A14, A16, LIMFUNC2:11;
hence left_improper_integral (f,a,c) = +infty by A12, A13, A26, Def3; :: thesis: