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