let a, c, d, b be real number ; :: thesis: for f, g being PartFunc of REAL ,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['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 PartFunc of REAL ,REAL ; :: thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['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 & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['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 A2: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & g is_integrable_on ['c,d'] & g | ['c,d'] is bounded ) by Th18;
c <= b by A1, XXREAL_0:2;
then ['c,b'] c= ['a,b'] by A1, Lm3;
then A3: ( ['c,b'] c= dom f & ['c,b'] c= dom g ) by A1, XBOOLE_1:1;
['c,d'] c= ['c,b'] by A1, Lm3;
then ( ['c,d'] c= dom f & ['c,d'] c= dom g ) by A3, XBOOLE_1:1;
hence f + g is_integrable_on ['c,d'] by A2, Th11; :: thesis: (f + g) | ['c,d'] is bounded
(f + g) | (['c,d'] /\ ['c,d']) is bounded by A2, RFUNCT_1:100;
hence (f + g) | ['c,d'] is bounded ; :: thesis: verum