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 ;
( A c= dom f & A c= dom g ) by ;
hence f + g is_integrable_on ['c,d'] by ; :: thesis: (f + g) | ['c,d'] is bounded
a <= d by ;
then ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by ;
then A3: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by ;
['c,d'] /\ ['c,d'] = ['c,d'] ;
hence (f + g) | ['c,d'] is bounded by ; :: thesis: verum