let f be PartFunc of REAL,REAL; :: thesis: for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] holds
for d being Real st d >= c holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
let b, c be Real; :: thesis: ( b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] implies for d being Real st d >= c holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) )
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f | ['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'] ; :: thesis: for d being Real st d >= c holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )

hereby :: thesis: verum

let d be Real; :: thesis: ( d >= c implies ( f is_integrable_on ['c,b₁'] & f | ['c,b₁'] is bounded ) )
assume A6: d >= c ; :: thesis: ( f is_integrable_on ['c,b₁'] & f | ['c,b₁'] is bounded )
then ['c,d'] = [.c,d.] by INTEGRA5:def 3;
then ['c,d'] c= [.c,+infty.[ by XXREAL_1:251;
then A7: ['c,d'] c= dom f by A2;
A8: ( ['c,b'] = [.c,b.] & ['c,d'] = [.c,d.] ) by A1, A6, INTEGRA5:def 3;

per cases ( d >= b or b > d ) ;

suppose A9: d >= b ; :: thesis: ( f is_integrable_on ['c,b₁'] & f | ['c,b₁'] is bounded )

then A10: ( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded ) by A4;
hence f is_integrable_on ['c,d'] by A9, A1, A7, A3, A5, INTEGR24:1; :: thesis: f | ['c,d'] is bounded
['b,d'] = [.b,d.] by A9, INTEGRA5:def 3;
then ['b,d'] \/ ['c,b'] = [.c,d.] by A9, A1, A8, XXREAL_1:165;
hence f | ['c,d'] is bounded by A10, A3, A8, RFUNCT_1:87; :: thesis: verum

end;

suppose A11: b > d ; :: thesis: ( f is_integrable_on ['c,b₁'] & f | ['c,b₁'] is bounded )

[.c,b.] c= [.c,+infty.[ by XXREAL_1:251;
then A12: ['c,b'] c= dom f by A2, A8;
d in ['c,b'] by A8, A11, A6, XXREAL_1:1;
hence f is_integrable_on ['c,d'] by A1, A3, A5, A12, INTEGRA6:17; :: thesis: f | ['c,d'] is bounded
thus f | ['c,d'] is bounded by A3, A11, A8, XXREAL_1:34, RFUNCT_1:74; :: thesis: verum

end;

end;

end;