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_right_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_right_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: ext_right_integral (f,a,b) = integral (f,a,b)
reconsider AB = [.a,b.[ as non empty Subset of REAL by A1, XXREAL_1:3;
deffunc H₁( Element of AB) -> Element of REAL = integral (f,a,$1);
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 number such that
A7: for x being set st x in ['a,b'] /\ (dom f) holds
abs (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
abs (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 abs (f . x) < M )
assume x in ['a,b'] ; :: thesis: abs (f . x) < M
hence abs (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 abs (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
( r < b & ( for r1 being Real st r < r1 & r1 < b & 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
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) )
assume 0 < g1 ; :: thesis: ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
then consider r being Real such that
A12: a < r and
A13: r < b and
A14: (b - r) * M < g1 by A1, A10, Th1;
take r ; :: thesis: ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
thus r < b by A13; :: thesis: for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1

now

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

end;

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

end;

A25: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) by A5, A6;
for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom Intf )

proof

let r be Element of REAL ; :: thesis: ( r < b implies ex g being Real st
( r < g & g < b & g in dom Intf ) )
assume A26: r < b ; :: thesis: ex g being Real st
( r < g & g < b & g in dom Intf )

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

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

reconsider g = a as Real ;
take g ; :: thesis: ( r < g & g < b & g in dom Intf )
thus ( r < g & g < b & g in dom Intf ) by A1, A6, A27, XXREAL_1:3; :: thesis: verum

end;

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

then A28: a - a <= r - a by XREAL_1:9;
reconsider g = r + ((b - r) / 2) as Real ;
take g ; :: thesis: ( r < g & g < b & g in dom Intf )
A29: 0 < b - r by A26, XREAL_1:50;
then (b - r) / 2 < b - r by XREAL_1:216;
then A30: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8;
r < g by A29, XREAL_1:29, XREAL_1:215;
then A31: r - (r - a) < g - 0 by A28, XREAL_1:14;
0 < (b - r) / 2 by A29, XREAL_1:215;
hence ( r < g & g < b & g in dom Intf ) by A6, A31, A30, XREAL_1:8, XXREAL_1:3; :: thesis: verum

end;

end;

end;

then A32: Intf is_left_convergent_in b by A11, LIMFUNC2:7;
then A33: integral (f,a,b) = lim_left (Intf,b) by A11, LIMFUNC2:41;
for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2, A3, A4, INTEGRA6:18;
then f is_right_ext_Riemann_integrable_on a,b by A6, A25, A32, Def1;
hence ext_right_integral (f,a,b) = integral (f,a,b) by A6, A25, A32, A33, Def3; :: thesis: verum