let f be PartFunc of REAL,REAL; :: thesis: for a, c being Real st ].a,c.] c= dom f & f is_left_improper_integrable_on a,c holds
for b being Real st a < b & b <= c holds
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
let a, c be Real; :: thesis: ( ].a,c.] c= dom f & f is_left_improper_integrable_on a,c implies for b being Real st a < b & b <= c holds
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) )
assume that
A1: ].a,c.] c= dom f and
A2: f is_left_improper_integrable_on a,c ; :: thesis: for b being Real st a < b & b <= c holds
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
let b be Real; :: thesis: ( a < b & b <= c implies for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) )
assume A3: ( a < b & b <= c ) ; :: thesis: for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
thus for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) :: thesis: verum

proof

let d be Real; :: thesis: ( a < d & d <= b implies ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) )
assume A4: ( a < d & d <= b ) ; :: thesis: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
then A5: ( a < d & d <= c ) by A3, XXREAL_0:2;
then A6: ( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded ) by A2;
A7: [.d,c.] = ['d,c'] by A4, A3, XXREAL_0:2, INTEGRA5:def 3;
then ['d,c'] c= ].a,c.] by A4, XXREAL_1:39;
then A8: ['d,c'] c= dom f by A1;
b in ['d,c'] by A7, A4, A3, XXREAL_1:1;
hence f is_integrable_on ['d,b'] by A6, A5, A8, INTEGRA6:17; :: thesis: f | ['d,b'] is bounded
[.d,b.] = ['d,b'] by A4, INTEGRA5:def 3;
hence f | ['d,b'] is bounded by A6, A3, A7, XXREAL_1:34, RFUNCT_1:74; :: thesis: verum

end;