let f be PartFunc of REAL,REAL; for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] holds
for d being Real st a < d & d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded )
let a, b, c be Real; ( a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] implies for d being Real st a < d & d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded ) )
assume that
A1:
( a < b & b <= c )
and
A2:
].a,c.] c= dom f
and
A3:
f | ['b,c'] is bounded
and
A4:
f is_left_improper_integrable_on a,b
and
A5:
f is_integrable_on ['b,c']
; for d being Real st a < d & d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded )
hereby verum
let d be
Real;
( a < d & d <= c implies ( f is_integrable_on ['b1,c'] & f | ['b1,c'] is bounded ) )assume A6:
(
a < d &
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= ].a,c.]
by A6, XXREAL_1:39;
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, A6;
hence
f is_integrable_on ['d,c']
by A9, A1, A7, A3, A5, Th1;
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= ].a,c.]
by A1, XXREAL_1:39;
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;