theorem Th12: :: INTEGRA6:12

for a, b being Real
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)) )