let f be PartFunc of REAL,REAL; :: thesis: 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; :: thesis: ( ].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 ; :: thesis: 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 :: thesis: verum

let c, d be Real; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;