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 A1, Th1, INTEGR20:19, XXREAL_0:2;
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:15; :: thesis: (f - g) | ['c,d'] is bounded
A3: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A1, A1X, Th1915b;
['c,d'] /\ ['c,d'] = ['c,d'] ;
hence (f - g) | ['c,d'] is bounded by A3, Th1935; :: thesis: verum