let a, b, c, d be Real; :: thesis: for f, g being PartFunc of REAL,REAL st a <= b & c <= d & 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 & c in ['a,b'] & d in ['a,b'] holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
let f, g be PartFunc of REAL,REAL; :: thesis: ( a <= b & c <= d & 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 & c in ['a,b'] & d in ['a,b'] implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) )
assume that
A1: a <= b and
A2: c <= d and
A3: f is_integrable_on ['a,b'] and
A4: g is_integrable_on ['a,b'] and
A5: f | ['a,b'] is bounded and
A6: g | ['a,b'] is bounded and
A7: ['a,b'] c= dom f and
A8: ['a,b'] c= dom g and
A9: ( c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A10: ( a <= c & d <= b ) by A9, XXREAL_1:1;
then A11: ( f is_integrable_on ['c,d'] & ['c,d'] c= dom f ) by A2, A3, A5, A7, Th18;
A12: ( g is_integrable_on ['c,d'] & ['c,d'] c= dom g ) by A2, A4, A6, A8, A10, Th18;
A13: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A2, A3, A4, A5, A6, A7, A8, A10, Th18;
then (f + g) | (['c,d'] /\ ['c,d']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) by A2, A11, A13, A12, Th11, Th12, RFUNCT_1:84; :: thesis: verum