let n be Element of NAT ; for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
let a, b, c, d be Real; for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL n); ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
assume A1:
( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] )
; integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
A2:
( - g is_integrable_on ['a,b'] & (- g) | ['a,b'] is bounded )
by A1, Th12;
A3:
dom g = dom (- g)
by NFCONT_4:def 3;
f - g = f + (- g)
by Lm1;
hence integral ((f - g),c,d) =
(integral (f,c,d)) + (integral ((- g),c,d))
by A1, A2, A3, Th27
.=
(integral (f,c,d)) - (integral (g,c,d))
by A1, Th26
;
verum