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
( f is_left_ext_Riemann_integrable_on a,b & 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 ( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) ) )
assume that
A1: a < b and
A2: ['a,b'] c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded ; :: thesis: ( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) )
reconsider AB = ].a,b.] as non empty Subset of REAL by A1, 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
A5: for x being Element of AB holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A6: dom Intf = AB by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
consider M0 being Real such that
A7: for x being object st x in ['a,b'] /\ (dom f) holds
|.(f . x).| <= M0 by A4, RFUNCT_1:73;
reconsider M = M0 + 1 as Real ;
A8: for x being Real st x in ['a,b'] holds
|.(f . x).| < M

proof

A9: ['a,b'] /\ (dom f) = ['a,b'] by A2, XBOOLE_1:28;
let x be Real; :: thesis: ( x in ['a,b'] implies |.(f . x).| < M )
assume x in ['a,b'] ; :: thesis: |.(f . x).| < M
hence |.(f . x).| < M by A7, A9, XREAL_1:39; :: 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 3;
then |.(f . a).| < M by A8;
then A10: 0 < M by COMPLEX1:46;
A11: 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) - (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
|.((Intf . r1) - (integral (f,a,b))).| < 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) - (integral (f,a,b))).| < g1 ) )
then consider r being Real such that
A12: a < r and
A13: r < b and
A14: (r - a) * M < g1 by A1, A10, INTEGR10:2;
reconsider r = r as Real ;
take r ; :: thesis: ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )
thus a < r by A12; :: thesis: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1

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

let r1 be Real; :: thesis: ( r1 < r & a < r1 & r1 in dom Intf implies |.((Intf . r1) - (integral (f,a,b))).| < g1 )
assume that
A15: r1 < r and
A16: a < r1 and
r1 in dom Intf ; :: thesis: |.((Intf . r1) - (integral (f,a,b))).| < g1
A17: r1 <= b by A13, A15, XXREAL_0:2;
then reconsider rr = r1 as Element of AB by A16, XXREAL_1:2;
A18: Intf . r1 = H₁(rr) by A5;
r1 in [.a,b.] by A16, XXREAL_1:1, A17;
then A19: r1 in ['a,b'] by A1, INTEGRA5:def 3;
r - a > r1 - a by A15, XREAL_1:9;
then A20: M * (r - a) > M * (r1 - a) by A10, XREAL_1:68;
A21: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
[.a,r1.] = ['a,r1'] by A16, INTEGRA5:def 3;
then ['a,r1'] c= ['a,b'] by A21, A17, XXREAL_1:34;
then A22: for x being Real st x in ['a,r1'] holds
|.(f . x).| <= M by A8;
a in ['a,b'] by A1, A21, XXREAL_1:1;
then |.(integral (f,a,r1)).| <= M * (r1 - a) by A1, A2, A3, A4, A16, A19, A22, INTEGRA6:23;
then A23: |.(integral (f,a,r1)).| < M * (r - a) by A20, XXREAL_0:2;
|.((Intf . r1) - (integral (f,a,b))).| = |.((integral (f,a,b)) - (Intf . r1)).| by COMPLEX1:60
.= |.(((integral (f,a,r1)) + (integral (f,r1,b))) - (integral (f,r1,b))).| by A1, A2, A3, A4, A18, A19, INTEGRA6:17
.= |.(integral (f,a,r1)).| ;
hence |.((Intf . r1) - (integral (f,a,b))).| < g1 by A14, A23, XXREAL_0:2; :: thesis: verum

end;

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

end;

A24: 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 A25: x in dom Intf ; :: thesis: Intf . x = integral (f,x,b)
reconsider x = x as Element of AB by A25, FUNCT_2:def 1;
Intf . x = H₁(x) by A5;
hence Intf . x = integral (f,x,b) ; :: thesis: verum

end;

A26: 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 A27: a < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom Intf )

per cases ( b < r or b >= r ) ;

suppose A28: 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 )
thus ( g < r & a < g & g in dom Intf ) by A1, A6, A28, XXREAL_1:2; :: thesis: verum

end;

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

reconsider g = r - ((r - a) / 2) as Real ;
take g ; :: thesis: ( g < r & a < g & g in dom Intf )
A30: 0 < r - a by A27, XREAL_1:50;
then - (r - a) < - ((r - a) / 2) by XREAL_1:24, XREAL_1:216;
then A31: (a - r) + r < (- ((r - a) / 2)) + r by XREAL_1:8;
g < r by A30, XREAL_1:44, XREAL_1:215;
then g <= b by A29, XXREAL_0:2;
hence ( g < r & a < g & g in dom Intf ) by A6, A30, A31, XREAL_1:44, XREAL_1:215, XXREAL_1:2; :: thesis: verum

end;

end;

end;

for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A2, A3, A4, INTEGRA6:18;
hence f is_left_ext_Riemann_integrable_on a,b by A6, A24, A26, A11, LIMFUNC2:10, INTEGR10:def 2; :: thesis: ext_left_integral (f,a,b) = integral (f,a,b)
thus ext_left_integral (f,a,b) = integral (f,a,b) by A1, A2, A3, A4, INTEGR10:13; :: thesis: verum