let a, b be Real; :: thesis: for f, g being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded holds
( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
let f, g be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded implies ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) )
assume that
A1: a <= b and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) ; :: thesis: ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
A3: ( integral ((f + g),a,b) = integral ((f + g),['a,b']) & integral ((f - g),a,b) = integral ((f - g),['a,b']) ) by A1, INTEGRA5:def 4;
( integral (f,a,b) = integral (f,['a,b']) & integral (g,a,b) = integral (g,['a,b']) ) by A1, INTEGRA5:def 4;
hence ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) by A2, A3, Th11; :: thesis: verum