let f be PartFunc of REAL,REAL; for b, c being Real st b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] holds
for d being Real st d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded )
let b, c be Real; ( b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] implies for d being Real st d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded ) )
assume that
A1:
b <= c
and
A2:
left_closed_halfline c c= dom f
and
A3:
f | ['b,c'] is bounded
and
A4:
f is_-infty_improper_integrable_on b
and
A5:
f is_integrable_on ['b,c']
; for d being Real st d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded )
hereby verum
let d be
Real;
( d <= c implies ( f is_integrable_on ['b1,c'] & f | ['b1,c'] is bounded ) )assume A6:
d <= c
;
( f is_integrable_on ['b1,c'] & f | ['b1,c'] is bounded )then
['d,c'] = [.d,c.]
by INTEGRA5:def 3;
then
['d,c'] c= ].-infty,c.]
by XXREAL_1:265;
then A7:
['d,c'] c= dom f
by A2;
A8:
(
['b,c'] = [.b,c.] &
['d,c'] = [.d,c.] )
by A1, A6, INTEGRA5:def 3;
per cases
( d <= b or b < d )
;
suppose A9:
d <= b
;
( f is_integrable_on ['b1,c'] & f | ['b1,c'] is bounded )then A10:
(
f is_integrable_on ['d,b'] &
f | ['d,b'] is
bounded )
by A4;
hence
f is_integrable_on ['d,c']
by A9, A1, A7, A3, A5, INTEGR24:1;
f | ['d,c'] is bounded
['d,b'] = [.d,b.]
by A9, INTEGRA5:def 3;
then
['d,b'] \/ ['b,c'] = [.d,c.]
by A9, A1, A8, XXREAL_1:165;
hence
f | ['d,c'] is
bounded
by A10, A3, A8, RFUNCT_1:87;
verum end; suppose A11:
b < d
;
( f is_integrable_on ['b1,c'] & f | ['b1,c'] is bounded )
[.b,c.] c= ].-infty,c.]
by XXREAL_1:265;
then A12:
['b,c'] c= dom f
by A2, A8;
d in ['b,c']
by A8, A11, A6, XXREAL_1:1;
hence
f is_integrable_on ['d,c']
by A1, A3, A5, A12, INTEGRA6:17;
f | ['d,c'] is bounded thus
f | ['d,c'] is
bounded
by A3, A11, A8, XXREAL_1:34, RFUNCT_1:74;
verum end;
end;