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_left_ext_Riemann_integrable_on c,d & ( a < c implies ext_left_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_left_ext_Riemann_integrable_on c,d & ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) ) ) )
assume A1: ( ].a,b.] c= dom f & 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_left_ext_Riemann_integrable_on c,d & ( a < c implies 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 & ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) ) ) )
assume that
A2: a <= c and
A3: c < d and
A4: d <= b ; :: thesis: ( f is_left_ext_Riemann_integrable_on c,d & ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) ) )
c < b by A3, A4, XXREAL_0:2;
then A5: f is_left_ext_Riemann_integrable_on c,b by A1, A2, Lm4;
].c,b.] c= ].a,b.] by A2, XXREAL_1:42;
then ].c,b.] c= dom f by A1;
hence f is_left_ext_Riemann_integrable_on c,d by A3, A4, A5, Th22; :: thesis: ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) )
thus ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) ) :: thesis: verum

proof

assume A6: a < c ; :: thesis: ext_left_integral (f,c,d) = integral (f,c,d)
a < d by A2, A3, XXREAL_0:2;
then f is_left_ext_Riemann_integrable_on a,d by A1, A4, Th22;
then A7: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) by A3, A6, INTEGR10:def 2;
['c,d'] = [.c,d.] by A3, INTEGRA5:def 3;
then ['c,d'] c= ].a,b.] by A4, A6, XXREAL_1:39;
then ['c,d'] c= dom f by A1;
hence ext_left_integral (f,c,d) = integral (f,c,d) by A3, A7, INTEGR10:13; :: thesis: verum

end;

end;