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 )
then a <= d by XXREAL_0:2;
then A1X: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by ;
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
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