let n be Element of NAT ; :: thesis: for a, b being Real
for f, g being PartFunc of REAL,() st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g 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 a, b be Real; :: thesis: for f, g being PartFunc of REAL,() st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g 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,(); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g 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 A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g ) ; :: 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)) )
A2: ( f + g is_integrable_on ['a,b'] & integral ((f + g),['a,b']) = (integral (f,['a,b'])) + (integral (g,['a,b'])) ) by ;
A3: ( f - g is_integrable_on ['a,b'] & integral ((f - g),['a,b']) = (integral (f,['a,b'])) - (integral (g,['a,b'])) ) by ;
A4: ['a,b'] = [.a,b.] by ;
thus integral ((f + g),a,b) = integral ((f + g),['a,b']) by
.= (integral (f,a,b)) + (integral (g,['a,b'])) by
.= (integral (f,a,b)) + (integral (g,a,b)) by ; :: thesis: integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b))
thus integral ((f - g),a,b) = integral ((f - g),['a,b']) by
.= (integral (f,a,b)) - (integral (g,['a,b'])) by
.= (integral (f,a,b)) - (integral (g,a,b)) by ; :: thesis: verum