let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st [.a,b.[ c= dom f & f is_right_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 & ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) )
let a, b be Real; :: thesis: ( [.a,b.[ c= dom f & f is_right_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 & ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) ) )
assume A1: ( [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b ) ; :: thesis: for c, d being Real st a <= c & c < d & d <= b holds
( f is_right_ext_Riemann_integrable_on c,d & ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) )

hereby :: thesis: verum

let c, d be Real; :: thesis: ( a <= c & c < d & d <= b implies ( f is_right_ext_Riemann_integrable_on c,d & ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) ) )
assume that
A2: a <= c and
A3: c < d and
A4: d <= b ; :: thesis: ( f is_right_ext_Riemann_integrable_on c,d & ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) )
a < d by A2, A3, XXREAL_0:2;
then A5: f is_right_ext_Riemann_integrable_on a,d by A1, A4, Lm6;
[.a,d.[ c= [.a,b.[ by A4, XXREAL_1:38;
then [.a,d.[ c= dom f by A1;
hence f is_right_ext_Riemann_integrable_on c,d by A2, A3, A5, Th25; :: thesis: ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) )
thus ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) :: thesis: verum

proof

assume A6: d < b ; :: thesis: ext_right_integral (f,c,d) = integral (f,c,d)
c < b by A3, A4, XXREAL_0:2;
then f is_right_ext_Riemann_integrable_on c,b by A1, A2, Th25;
then A7: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) by A3, A6, INTEGR10:def 1;
['c,d'] = [.c,d.] by A3, INTEGRA5:def 3;
then ['c,d'] c= [.a,b.[ by A2, A6, XXREAL_1:43;
then ['c,d'] c= dom f by A1;
hence ext_right_integral (f,c,d) = integral (f,c,d) by A3, A7, INTEGR10:12; :: thesis: verum

end;

end;