let a, b, c, d be Real; :: thesis: for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((- f),c,d) = - (integral (f,c,d))
let Y be RealBanachSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((- f),c,d) = - (integral (f,c,d))
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((- f),c,d) = - (integral (f,c,d)) )
assume A1: ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral ((- f),c,d) = - (integral (f,c,d))
A2: - f = (- 1) (#) f by VFUNCT_1:23;
(- 1) * (integral (f,c,d)) = - (integral (f,c,d)) by RLVECT_1:16;
hence integral ((- f),c,d) = - (integral (f,c,d)) by A1, A2, Th1925; :: thesis: verum