let a, b, c, d be Real; :: thesis: for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
let f, g be PartFunc of REAL,REAL; :: thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) )
assume that
A1: a <= c and
A2: ( c <= d & d <= b ) and
A3: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) and
A4: ['a,b'] c= dom f and
A5: ['a,b'] c= dom g ; :: thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
A6: ['c,d'] c= ['c,b'] by A2, Lm3;
A7: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A1, A2, A3, A4, A5, Th18;
c <= b by A2, XXREAL_0:2;
then A8: ['c,b'] c= ['a,b'] by A1, Lm3;
then ['c,b'] c= dom f by A4;
then A9: ['c,d'] c= dom f by A6;
['c,b'] c= dom g by A5, A8;
then A10: ['c,d'] c= dom g by A6;
( f is_integrable_on ['c,d'] & g is_integrable_on ['c,d'] ) by A1, A2, A3, A4, A5, Th18;
hence f + g is_integrable_on ['c,d'] by A7, A9, A10, Th11; :: thesis: (f + g) | ['c,d'] is bounded
(f + g) | (['c,d'] /\ ['c,d']) is bounded by A7, RFUNCT_1:83;
hence (f + g) | ['c,d'] is bounded ; :: thesis: verum