let n be Element of NAT ; for a, b being Real
for f, g being PartFunc of REAL,(REAL-NS n) 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; for f, g being PartFunc of REAL,(REAL-NS n) 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,(REAL-NS n); ( 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 )
; ( 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 A1, INTEGR18:14;
A3:
( f - g is_integrable_on ['a,b'] & integral ((f - g),['a,b']) = (integral (f,['a,b'])) - (integral (g,['a,b'])) )
by A1, INTEGR18:15;
A4:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
thus integral ((f + g),a,b) =
integral ((f + g),['a,b'])
by A4, INTEGR18:16
.=
(integral (f,a,b)) + (integral (g,['a,b']))
by A4, A2, INTEGR18:16
.=
(integral (f,a,b)) + (integral (g,a,b))
by A4, INTEGR18:16
; 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 A4, INTEGR18:16
.=
(integral (f,a,b)) - (integral (g,['a,b']))
by A4, A3, INTEGR18:16
.=
(integral (f,a,b)) - (integral (g,a,b))
by A4, INTEGR18:16
; verum