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

per cases then ( a = c or a < c ) by XXREAL_0:1;

suppose a = c ; :: thesis: f is_left_ext_Riemann_integrable_on c,b

hence f is_left_ext_Riemann_integrable_on c,b by A2; :: thesis: verum

end;

suppose A4: a < c ; :: thesis: f is_left_ext_Riemann_integrable_on c,b

then [.c,b.] c= ].a,b.] by XXREAL_1:39;
then ['c,b'] c= ].a,b.] by A3, INTEGRA5:def 3;
then A5: ['c,b'] c= dom f by A1;
( f is_integrable_on ['c,b'] & f | ['c,b'] is bounded ) by A2, A3, A4, INTEGR10:def 2;
hence f is_left_ext_Riemann_integrable_on c,b by A3, A5, Lm3; :: thesis: verum

end;

end;