let a, b, c, d be Real; :: thesis: for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['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 Y be RealBanachSpace; :: thesis: for f, g being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['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 continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & c <= d & ['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 & c <= d & ['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))
reconsider A = ['c,d'] as non empty closed_interval Subset of REAL ;
['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then ( a <= c & c <= b & a <= d & d <= b ) by A1, XXREAL_1:1;
then A4: ( f is_integrable_on A & g is_integrable_on A ) by A1, Th1909;
( c = min (c,d) & d = max (c,d) ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;
then ['c,d'] c= ['a,b'] by A1, Lm2;
then A5: ( A c= dom f & A c= dom g ) by A1;
( integral ((f - g),A) = integral ((f - g),c,d) & integral (f,A) = integral (f,c,d) & integral (g,A) = integral (g,c,d) ) by A1, INTEGR18:def 9;
hence integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) by A5, A4, INTEGR18:15; :: thesis: verum