let f be PartFunc of REAL,REAL; 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; ( 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']
; for d being Real st d >= c holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
hereby verum
let d be
Real;
( d >= c implies ( f is_integrable_on ['c,b1'] & f | ['c,b1'] is bounded ) )assume A6:
d >= c
;
( f is_integrable_on ['c,b1'] & f | ['c,b1'] 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
;
( f is_integrable_on ['c,b1'] & f | ['c,b1'] 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;
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;
verum end; suppose A11:
b > d
;
( f is_integrable_on ['c,b1'] & f | ['c,b1'] 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;
f | ['c,d'] is bounded thus
f | ['c,d'] is
bounded
by A3, A11, A8, XXREAL_1:34, RFUNCT_1:74;
verum end; end;
end;