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

let d be Real; :: thesis:
assume A4: ( b <= d & d < c ) ; :: thesis:
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:
[.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:

end;