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

proof

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

end;