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 d being Real st a < d & d <= b holds
f is_right_ext_Riemann_integrable_on a,d
let a, b be Real; :: thesis: ( [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b implies for d being Real st a < d & d <= b holds
f is_right_ext_Riemann_integrable_on a,d )
assume that
A1: [.a,b.[ c= dom f and
A2: f is_right_ext_Riemann_integrable_on a,b ; :: thesis: for d being Real st a < d & d <= b holds
f is_right_ext_Riemann_integrable_on a,d
let d be Real; :: thesis: ( a < d & d <= b implies f is_right_ext_Riemann_integrable_on a,d )
assume A3: ( a < d & d <= b ) ; :: thesis: f is_right_ext_Riemann_integrable_on a,d

per cases then ( d = b or d < b ) by XXREAL_0:1;

suppose d = b ; :: thesis: f is_right_ext_Riemann_integrable_on a,d

hence f is_right_ext_Riemann_integrable_on a,d by A2; :: thesis: verum

end;

suppose A4: d < b ; :: thesis: f is_right_ext_Riemann_integrable_on a,d

then [.a,d.] c= [.a,b.[ by XXREAL_1:43;
then ['a,d'] c= [.a,b.[ by A3, INTEGRA5:def 3;
then A5: ['a,d'] c= dom f by A1;
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2, A3, A4, INTEGR10:def 1;
hence f is_right_ext_Riemann_integrable_on a,d by A3, A5, Lm5; :: thesis: verum

end;

end;