let a, b, c, d be Real; 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; 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; ( 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'] )
; 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; verum