let a, b, c, d be Real; :: thesis: for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['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 Y be RealBanachSpace; :: thesis: for f, g being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['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 continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= c & c <= d & d <= b & ['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 A1: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g ) ; :: thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL ;
A2: ( f is_integrable_on A & g is_integrable_on A ) by A1, Th1909;
( A c= dom f & A c= dom g ) by A1, INTEGR19:2;
hence f + g is_integrable_on ['c,d'] by A2, INTEGR18:14; :: thesis: (f + g) | ['c,d'] is bounded
a <= d by A1, XXREAL_0:2;
then ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by A1, Th1, XXREAL_0:2;
then A3: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A1, Th1915b;
['c,d'] /\ ['c,d'] = ['c,d'] ;
hence (f + g) | ['c,d'] is bounded by A3, Th1935; :: thesis: verum