let f be PartFunc of REAL ,REAL ; :: thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
ext_left_integral f,a,b = integral f,a,b
let a, b be Real; :: thesis: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ext_left_integral f,a,b = integral f,a,b )
assume A1: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ; :: thesis: ext_left_integral f,a,b = integral f,a,b
A2: for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A1, INTEGRA6:18;
reconsider AB = ].a,b.] as non empty Subset of REAL by A1, XXREAL_1:2;
deffunc H₁( Element of AB) -> Element of REAL = integral f,$1,b;
consider Intf being Function of AB,REAL such that
A3: for x being Element of AB holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A4: dom Intf = AB by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL ,REAL by RELSET_1:13;
A5: for x being Real st x in dom Intf holds
Intf . x = integral f,x,b by A3, A4;
A6: 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 Element of REAL ; :: thesis: ( a < r implies ex g being Real st
( g < r & a < g & g in dom Intf ) )
assume A7: a < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom Intf )

per cases ( b < r or not b < r ) ;

suppose A8: b < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom Intf )

reconsider g = b as Real ;
take g ; :: thesis: ( g < r & a < g & g in dom Intf )
g in ].a,b.] by A1, XXREAL_1:2;
hence ( g < r & a < g & g in dom Intf ) by A8, A1, FUNCT_2:def 1; :: thesis: verum

end;

suppose A9: not b < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom Intf )

reconsider g = a + ((r - a) / 2) as Real ;
take g ; :: thesis: ( g < r & a < g & g in dom Intf )
0 < r - a by A7, XREAL_1:52;
then A10: ( 0 < (r - a) / 2 & (r - a) / 2 < r - a ) by XREAL_1:217, XREAL_1:218;
then A11: a < g by XREAL_1:31;
A12: ((r - a) / 2) + a < (r - a) + a by A10, XREAL_1:10;
g < b by A9, A12, XXREAL_0:2;
hence ( g < r & a < g & g in dom Intf ) by A11, A12, A4, XXREAL_1:2; :: thesis: verum

end;

end;

end;

consider M0 being real number such that
A14: for x being set st x in ['a,b'] /\ (dom f) holds
abs (f . x) <= M0 by RFUNCT_1:90, A1;
reconsider M = M0 + 1 as Real ;
A15: ( 0 < M & ( for x being Real st x in ['a,b'] holds
abs (f . x) <= M ) )

proof

A16: for x being Real st x in ['a,b'] holds
abs (f . x) < M

proof

let x be Real; :: thesis: ( x in ['a,b'] implies abs (f . x) < M )
assume A17: x in ['a,b'] ; :: thesis: abs (f . x) < M
['a,b'] /\ (dom f) = ['a,b'] by A1, XBOOLE_1:28;
hence abs (f . x) < M by XREAL_1:41, A17, A14; :: thesis: verum

end;

a in { r where r is Real : ( a <= r & r <= b ) } by A1;
then a in [.a,b.] by RCOMP_1:def 1;
then a in ['a,b'] by A1, INTEGRA5:def 4;
then abs (f . a) < M by A16;
hence ( 0 < M & ( for x being Real st x in ['a,b'] holds
abs (f . x) <= M ) ) by A16, COMPLEX1:132; :: thesis: verum

end;

A20: 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
abs ((Intf . r1) - (integral f,a,b)) < 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
abs ((Intf . r1) - (integral f,a,b)) < g1 ) ) )
assume A21: 0 < g1 ; :: thesis: ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral f,a,b)) < g1 ) )
consider r being Real such that
A22: ( a < r & r < b & (r - a) * M < g1 ) by A15, A21, A1, Th2;
take r ; :: thesis: ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral f,a,b)) < g1 ) )
thus a < r by A22; :: thesis: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral f,a,b)) < g1

now

let r1 be Real; :: thesis: ( a < r1 & r1 < r & r1 in dom Intf implies abs ((Intf . r1) - (integral f,a,b)) < g1 )
assume A23: ( a < r1 & r1 < r & r1 in dom Intf ) ; :: thesis: abs ((Intf . r1) - (integral f,a,b)) < g1
then A24: Intf . r1 = integral f,r1,b by A3, A4;
A25: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
A26: r1 <= b by A23, A22, XXREAL_0:2;
A27: r1 in ['a,b'] by A25, A23, A26, XXREAL_1:1;
A28: abs ((Intf . r1) - (integral f,a,b)) = abs ((integral f,a,b) - (Intf . r1)) by COMPLEX1:146
.= abs (((integral f,a,r1) + (integral f,r1,b)) - (integral f,r1,b)) by A1, INTEGRA6:17, A24, A27
.= abs (integral f,a,r1) ;
A29: a in ['a,b'] by A1, XXREAL_1:1, A25;
A30: [.a,r1.] = ['a,r1'] by A23, INTEGRA5:def 4;
['a,r1'] c= ['a,b'] by A25, A30, A26, XXREAL_1:34;
then for x being real number st x in ['a,r1'] holds
abs (f . x) <= M by A15;
then A31: abs (integral f,a,r1) <= M * (r1 - a) by A1, A23, A27, A29, INTEGRA6:23;
r1 - a < r - a by A23, XREAL_1:16;
then M * (r1 - a) < M * (r - a) by A15, XREAL_1:70;
then abs (integral f,a,r1) < M * (r - a) by A31, XXREAL_0:2;
hence abs ((Intf . r1) - (integral f,a,b)) < g1 by A28, A22, XXREAL_0:2; :: thesis: verum

end;

hence for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral f,a,b)) < g1 ; :: thesis: verum

end;

then A32: Intf is_right_convergent_in a by A6, LIMFUNC2:16;
then A33: integral f,a,b = lim_right Intf,a by A20, LIMFUNC2:50;
f is_left_ext_Riemann_integrable_on a,b by A2, A4, A5, A32, Def2;
hence ext_left_integral f,a,b = integral f,a,b by A4, A5, A32, A33, Def4; :: thesis: verum