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_left_ext_Riemann_integrable_on c,d & ext_left_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_left_ext_Riemann_integrable_on c,d & ext_left_integral (f,c,d) = integral (f,c,d) ) )
assume that
A1: [.a,b.[ c= dom f and
A2: 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_left_ext_Riemann_integrable_on c,d & ext_left_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_left_ext_Riemann_integrable_on c,d & ext_left_integral (f,c,d) = integral (f,c,d) ) )
assume that
A3: ( a <= c & c < d ) and
A4: d < b ; :: thesis: ( f is_left_ext_Riemann_integrable_on c,d & ext_left_integral (f,c,d) = integral (f,c,d) )
A5: a < d by A3, XXREAL_0:2;
then ( ['a,d'] = [.a,d.] & ['a,b'] = [.a,b.] & ['c,d'] = [.c,d.] ) by A3, A4, XXREAL_0:2, INTEGRA5:def 3;
then ( ['a,d'] c= [.a,b.[ & ['c,d'] c= [.a,b.[ ) by A4, A3, XXREAL_1:43;
then A6: ( ['a,d'] c= dom f & ['c,d'] c= dom f ) by A1;
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A4, A5, A2, INTEGR10:def 1;
then A7: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) by A3, A6, INTEGRA6:18;
hence f is_left_ext_Riemann_integrable_on c,d by A3, A6, Th18; :: thesis: ext_left_integral (f,c,d) = integral (f,c,d)
thus ext_left_integral (f,c,d) = integral (f,c,d) by A3, A6, A7, Th18; :: thesis: verum

end;