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

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