let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds

( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )

let f be PartFunc of REAL,REAL; :: thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) )

assume that

A1: a <= c and

A2: c <= d and

A3: d <= b and

A4: f is_integrable_on ['a,b'] and

A5: f | ['a,b'] is bounded and

A6: ['a,b'] c= dom f ; :: thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )

a <= d by A1, A2, XXREAL_0:2;

then A7: a <= b by A3, XXREAL_0:2;

A8: c <= b by A2, A3, XXREAL_0:2;

then c in ['a,b'] by A1, Lm3;

then A9: f is_integrable_on ['c,b'] by A4, A5, A6, A7, Th17;

A10: d in ['c,b'] by A2, A3, Lm3;

A11: ['c,b'] c= ['a,b'] by A1, A8, Lm3;

then ( ['c,b'] c= dom f & f | ['c,b'] is bounded ) by A5, A6, RFUNCT_1:74;

hence f is_integrable_on ['c,d'] by A8, A10, A9, Th17; :: thesis: ( f | ['c,d'] is bounded & ['c,d'] c= dom f )

['c,d'] c= ['c,b'] by A2, A3, Lm3;

then A12: ['c,d'] c= ['a,b'] by A11;

hence f | ['c,d'] is bounded by A5, RFUNCT_1:74; :: thesis: ['c,d'] c= dom f

thus ['c,d'] c= dom f by A6, A12; :: thesis: verum

( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )

let f be PartFunc of REAL,REAL; :: thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) )

assume that

A1: a <= c and

A2: c <= d and

A3: d <= b and

A4: f is_integrable_on ['a,b'] and

A5: f | ['a,b'] is bounded and

A6: ['a,b'] c= dom f ; :: thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )

a <= d by A1, A2, XXREAL_0:2;

then A7: a <= b by A3, XXREAL_0:2;

A8: c <= b by A2, A3, XXREAL_0:2;

then c in ['a,b'] by A1, Lm3;

then A9: f is_integrable_on ['c,b'] by A4, A5, A6, A7, Th17;

A10: d in ['c,b'] by A2, A3, Lm3;

A11: ['c,b'] c= ['a,b'] by A1, A8, Lm3;

then ( ['c,b'] c= dom f & f | ['c,b'] is bounded ) by A5, A6, RFUNCT_1:74;

hence f is_integrable_on ['c,d'] by A8, A10, A9, Th17; :: thesis: ( f | ['c,d'] is bounded & ['c,d'] c= dom f )

['c,d'] c= ['c,b'] by A2, A3, Lm3;

then A12: ['c,d'] c= ['a,b'] by A11;

hence f | ['c,d'] is bounded by A5, RFUNCT_1:74; :: thesis: ['c,d'] c= dom f

thus ['c,d'] c= dom f by A6, A12; :: thesis: verum