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 ;
then A7: a <= b by ;
A8: c <= b by ;
then c in ['a,b'] by ;
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 ;
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 ; :: thesis: ['c,d'] c= dom f
thus ['c,d'] c= dom f by ; :: thesis: verum