let f be PartFunc of REAL,REAL; :: thesis: for c being Real st left_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 ['d,b'] & f | ['d,b'] is bounded )
let c be Real; :: thesis: ( left_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 ['d,b'] & f | ['d,b'] is bounded ) )
assume that
A1: left_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 ['d,b'] & f | ['d,b'] is bounded )
let b be Real; :: thesis: ( b <= c implies for d being Real st d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) )
assume A3: b <= c ; :: thesis: for d being Real st d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
thus for d being Real st d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) :: thesis: verum

proof

let d be Real; :: thesis: ( d <= b implies ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) )
assume A4: d <= b ; :: thesis: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
then A5: 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= ].-infty,c.] by XXREAL_1:265;
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;