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 A1: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ; :: thesis: ext_right_integral f,a,b = integral f,a,b
A2: for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A1, INTEGRA6:18;
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
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,a,x by A3, A4;
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 A7: 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 A8: 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 A8, A4, A1, XXREAL_1:3; :: thesis: verum

end;

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

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

end;

end;

end;

consider M0 being real number such that
A13: 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 ;
A14: ( 0 < M & ( for x being Real st x in ['a,b'] holds
abs (f . x) <= M ) )

proof

A15: 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 A16: x in ['a,b'] ; :: thesis: abs (f . x) < M
A17: ['a,b'] /\ (dom f) = ['a,b'] by A1, XBOOLE_1:28;
thus abs (f . x) < M by A17, A16, A13, XREAL_1:41; :: 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 A15;
hence ( 0 < M & ( for x being Real st x in ['a,b'] holds
abs (f . x) <= M ) ) by A15, COMPLEX1:132; :: thesis: verum

end;

A19: 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 A20: 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 ) )
consider r being Real such that
A21: ( a < r & r < b & (b - r) * M < g1 ) by A14, A20, A1, 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 A21; :: 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 A22: ( r < r1 & r1 < b & r1 in dom Intf ) ; :: thesis: abs ((Intf . r1) - (integral f,a,b)) < g1
then A23: Intf . r1 = integral f,a,r1 by A3, A4;
A24: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
A25: a <= r1 by A21, A22, XXREAL_0:2;
r1 in [.a,b.] by A22, A25, XXREAL_1:1;
then A26: r1 in ['a,b'] by A1, INTEGRA5:def 4;
A27: 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,a,r1)) by A1, INTEGRA6:17, A23, A26
.= abs (integral f,r1,b) ;
A28: b in ['a,b'] by A1, XXREAL_1:1, A24;
A29: [.r1,b.] = ['r1,b'] by A22, INTEGRA5:def 4;
['r1,b'] c= ['a,b'] by A24, A29, A25, XXREAL_1:34;
then for x being real number st x in ['r1,b'] holds
abs (f . x) <= M by A14;
then A30: abs (integral f,r1,b) <= M * (b - r1) by A1, A22, A26, A28, INTEGRA6:23;
b - r1 < b - r by A22, XREAL_1:17;
then M * (b - r1) < M * (b - r) by A14, XREAL_1:70;
then abs (integral f,r1,b) < M * (b - r) by A30, XXREAL_0:2;
hence abs ((Intf . r1) - (integral f,a,b)) < g1 by A21, A27, 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;

then A31: Intf is_left_convergent_in b by A6, LIMFUNC2:13;
then A32: integral f,a,b = lim_left Intf,b by A19, LIMFUNC2:49;
f is_right_ext_Riemann_integrable_on a,b by A2, A4, A5, A31, Def1;
hence ext_right_integral f,a,b = integral f,a,b by A4, A5, A31, A32, Def3; :: thesis: verum