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