let a, b be real number ; :: 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 5;
( integral f,a,b = integral f,['a,b'] & integral g,a,b = integral g,['a,b'] ) by A1, INTEGRA5:def 5;
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