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_{1}( Element of AB) -> Element of REAL = In ((integral (f,a,$1)),REAL);

consider Intf being Function of AB,REAL such that

A5: for x being Element of AB holds Intf . x = H_{1}(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

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

( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds

|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )

Intf . x = integral (f,a,x)

ex g being Real st

( r < g & g < b & g in dom Intf )

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, A24, A32;

hence ext_right_integral (f,a,b) = integral (f,a,b) by A6, A24, A32, A33, Def3; :: thesis: verum

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

consider Intf being Function of AB,REAL such that

A5: for x being Element of AB holds Intf . x = H

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

a in { r where r is Real : ( a <= r & r <= b ) }
by A1;
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;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

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

( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds

|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )

proof

A24:
for x being Real st x in dom Intf holds
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

|.((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

|.((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;

reconsider r = r as Real ;

take r ; :: thesis: ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds

|.((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

|.((Intf . r1) - (integral (f,a,b))).| < g1

|.((Intf . r1) - (integral (f,a,b))).| < g1 ; :: thesis: verum

end;( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds

|.((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

|.((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;

reconsider r = r as Real ;

take r ; :: thesis: ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds

|.((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

|.((Intf . r1) - (integral (f,a,b))).| < g1

now :: thesis: for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds

|.((Intf . r1) - (integral (f,a,b))).| < g1

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

let r1 be Real; :: thesis: ( r < r1 & r1 < b & r1 in dom Intf implies |.((Intf . r1) - (integral (f,a,b))).| < g1 )

assume that

A15: r < r1 and

A16: r1 < b and

r1 in dom Intf ; :: thesis: |.((Intf . r1) - (integral (f,a,b))).| < g1

A17: a <= r1 by A12, A15, XXREAL_0:2;

then reconsider rr = r1 as Element of AB by A16, XXREAL_1:3;

A18: Intf . r1 = H_{1}(rr)
by A5;

r1 in [.a,b.] by A16, XXREAL_1:1, A17;

then A19: r1 in ['a,b'] by A1, INTEGRA5:def 3;

b - r1 < b - r by A15, XREAL_1:15;

then A20: M * (b - r1) < M * (b - r) by A10, XREAL_1:68;

A21: ['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 A21, A17, XXREAL_1:34;

then A22: for x being Real st x in ['r1,b'] holds

|.(f . x).| <= M by A8;

b in ['a,b'] by A1, A21, XXREAL_1:1;

then |.(integral (f,r1,b)).| <= M * (b - r1) by A1, A2, A3, A4, A16, A19, A22, INTEGRA6:23;

then A23: |.(integral (f,r1,b)).| < M * (b - r) 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,a,r1))).| by A1, A2, A3, A4, A18, A19, INTEGRA6:17

.= |.(integral (f,r1,b)).| ;

hence |.((Intf . r1) - (integral (f,a,b))).| < g1 by A14, A23, XXREAL_0:2; :: thesis: verum

end;assume that

A15: r < r1 and

A16: r1 < b and

r1 in dom Intf ; :: thesis: |.((Intf . r1) - (integral (f,a,b))).| < g1

A17: a <= r1 by A12, A15, XXREAL_0:2;

then reconsider rr = r1 as Element of AB by A16, XXREAL_1:3;

A18: Intf . r1 = H

r1 in [.a,b.] by A16, XXREAL_1:1, A17;

then A19: r1 in ['a,b'] by A1, INTEGRA5:def 3;

b - r1 < b - r by A15, XREAL_1:15;

then A20: M * (b - r1) < M * (b - r) by A10, XREAL_1:68;

A21: ['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 A21, A17, XXREAL_1:34;

then A22: for x being Real st x in ['r1,b'] holds

|.(f . x).| <= M by A8;

b in ['a,b'] by A1, A21, XXREAL_1:1;

then |.(integral (f,r1,b)).| <= M * (b - r1) by A1, A2, A3, A4, A16, A19, A22, INTEGRA6:23;

then A23: |.(integral (f,r1,b)).| < M * (b - r) 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,a,r1))).| by A1, A2, A3, A4, A18, A19, INTEGRA6:17

.= |.(integral (f,r1,b)).| ;

hence |.((Intf . r1) - (integral (f,a,b))).| < g1 by A14, A23, XXREAL_0:2; :: thesis: verum

|.((Intf . r1) - (integral (f,a,b))).| < g1 ; :: thesis: verum

Intf . x = integral (f,a,x)

proof

for r being Real st r < b holds
let x be Real; :: thesis: ( x in dom Intf implies Intf . x = integral (f,a,x) )

assume A25: x in dom Intf ; :: thesis: Intf . x = integral (f,a,x)

dom Intf = AB by FUNCT_2:def 1;

then reconsider x = x as Element of AB by A25;

Intf . x = H_{1}(x)
by A5;

hence Intf . x = integral (f,a,x) ; :: thesis: verum

end;assume A25: x in dom Intf ; :: thesis: Intf . x = integral (f,a,x)

dom Intf = AB by FUNCT_2:def 1;

then reconsider x = x as Element of AB by A25;

Intf . x = H

hence Intf . x = integral (f,a,x) ; :: thesis: verum

ex g being Real st

( r < g & g < b & g in dom Intf )

proof

then A32:
Intf is_left_convergent_in b
by A11, LIMFUNC2:7;
let r be 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 )

end;( 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 )
;

end;

suppose A27:
r < a
; :: thesis: ex g being Real st

( r < g & g < b & g in dom Intf )

( 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;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

suppose
not r < a
; :: thesis: ex g being Real st

( r < g & g < b & g in dom Intf )

( 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;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

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, A24, A32;

hence ext_right_integral (f,a,b) = integral (f,a,b) by A6, A24, A32, A33, Def3; :: thesis: verum