let a, c, d, b be real number ; :: 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 & c <= d & d <= b ) and
A2: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and
A3: ['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, XXREAL_0:2;
then A4: ( a <= b & c <= b ) by A1, XXREAL_0:2;
then A5: ( c in ['a,b'] & d in ['c,b'] ) by A1, Lm3;
A6: ['c,b'] c= ['a,b'] by A1, A4, Lm3;
then A7: ['c,b'] c= dom f by A3, XBOOLE_1:1;
( f is_integrable_on ['c,b'] & f | ['c,b'] is bounded ) by A2, A3, A4, A5, A6, Th17, RFUNCT_1:91;
hence f is_integrable_on ['c,d'] by A4, A5, A7, Th17; :: thesis: ( f | ['c,d'] is bounded & ['c,d'] c= dom f )
['c,d'] c= ['c,b'] by A1, Lm3;
then A8: ['c,d'] c= ['a,b'] by A6, XBOOLE_1:1;
hence f | ['c,d'] is bounded by A2, RFUNCT_1:91; :: thesis: ['c,d'] c= dom f
thus ['c,d'] c= dom f by A3, A8, XBOOLE_1:1; :: thesis: verum