let f be PartFunc of REAL,REAL; :: thesis: for a, c being Real st [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c holds
for b being Real st a <= b & b < c holds
for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded )
let a, c be Real; :: thesis: ( [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c implies for b being Real st a <= b & b < c holds
for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded ) )
assume that
A1: [.a,c.[ c= dom f and
A2: f is_right_improper_integrable_on a,c ; :: thesis: for b being Real st a <= b & b < c holds
for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded )
let b be Real; :: thesis: ( a <= b & b < c implies for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded ) )
assume A3: ( a <= b & b < c ) ; :: thesis: for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded )
thus for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded ) :: thesis: verum

proof

let d be Real; :: thesis: ( b <= d & d < c implies ( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded ) )
assume A4: ( b <= d & d < c ) ; :: thesis: ( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded )
then A5: ( a <= d & d < c ) by A3, XXREAL_0:2;
then A6: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2;
A7: [.a,d.] = ['a,d'] by A4, A3, XXREAL_0:2, INTEGRA5:def 3;
then ['a,d'] c= [.a,c.[ by A4, XXREAL_1:43;
then A8: ['a,d'] c= dom f by A1;
b in ['a,d'] by A7, A4, A3, XXREAL_1:1;
hence f is_integrable_on ['b,d'] by A6, A5, A8, INTEGRA6:17; :: thesis: f | ['b,d'] is bounded
[.b,d.] = ['b,d'] by A4, INTEGRA5:def 3;
hence f | ['b,d'] is bounded by A6, A3, A7, XXREAL_1:34, RFUNCT_1:74; :: thesis: verum

end;