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

( 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