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 & ['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 & ['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 & ['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 & ['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))
per cases ( not c <= d or c <= d ) ;
suppose A2: not c <= d ; :: thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
then ( d = min (c,d) & c = max (c,d) ) by XXREAL_0:def 9, XXREAL_0:def 10;
then ['d,c'] c= ['a,b'] by A1, Lm2;
then A7: ( ['d,c'] c= dom f & ['d,c'] c= dom g ) by A1;
then ['d,c'] c= (dom f) /\ (dom g) by XBOOLE_1:19;
then ['d,c'] c= dom (f - g) by VFUNCT_1:def 2;
then A11: ( integral ((f - g),c,d) = - (integral ((f - g),d,c)) & integral (f,c,d) = - (integral (f,d,c)) & integral (g,c,d) = - (integral (g,d,c)) ) by A2, A7, Th1947;
integral ((f - g),d,c) = (integral (f,d,c)) - (integral (g,d,c)) by A1, A2, Th1928;
then integral ((f - g),c,d) = (integral (g,d,c)) + (integral (f,c,d)) by A11, RLVECT_1:33;
hence integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) by A11; :: thesis: verum
end;
suppose c <= d ; :: thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
hence integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) by A1, Th1928; :: thesis: verum
end;
end;