let n be Element of NAT ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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'] ) ; :: thesis: 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 ;
:: thesis: verum