let f be PartFunc of REAL,REAL; for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for c, d being Real st a < c & c < d & d <= b holds
( f is_right_ext_Riemann_integrable_on c,d & ext_right_integral (f,c,d) = integral (f,c,d) )
let a, b be Real; ( ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b implies for c, d being Real st a < c & c < d & d <= b holds
( f is_right_ext_Riemann_integrable_on c,d & ext_right_integral (f,c,d) = integral (f,c,d) ) )
assume that
A1:
].a,b.] c= dom f
and
A2:
f is_left_ext_Riemann_integrable_on a,b
; for c, d being Real st a < c & c < d & d <= b holds
( f is_right_ext_Riemann_integrable_on c,d & ext_right_integral (f,c,d) = integral (f,c,d) )
hereby verum
let c,
d be
Real;
( a < c & c < d & d <= b implies ( f is_right_ext_Riemann_integrable_on c,d & ext_right_integral (f,c,d) = integral (f,c,d) ) )assume that A3:
a < c
and A4:
(
c < d &
d <= b )
;
( f is_right_ext_Riemann_integrable_on c,d & ext_right_integral (f,c,d) = integral (f,c,d) )A5:
c < b
by A4, XXREAL_0:2;
then
(
['c,b'] = [.c,b.] &
['a,b'] = [.a,b.] &
['c,d'] = [.c,d.] )
by A3, A4, XXREAL_0:2, INTEGRA5:def 3;
then
(
['c,b'] c= ].a,b.] &
['c,d'] c= ].a,b.] )
by A4, A3, XXREAL_1:39;
then A6:
(
['c,b'] c= dom f &
['c,d'] c= dom f )
by A1;
(
f is_integrable_on ['c,b'] &
f | ['c,b'] is
bounded )
by A3, A5, A2, INTEGR10:def 2;
then A7:
(
f is_integrable_on ['c,d'] &
f | ['c,d'] is
bounded )
by A4, A6, INTEGRA6:18;
hence
f is_right_ext_Riemann_integrable_on c,
d
by A4, A6, Th19;
ext_right_integral (f,c,d) = integral (f,c,d)thus
ext_right_integral (
f,
c,
d)
= integral (
f,
c,
d)
by A4, A6, A7, Th19;
verum
end;