let X be RealNormSpace; :: thesis: for A being closed-interval Subset of REAL
for f, h being Function of A,the carrier of X st h = - f & f is integrable holds
( h is integrable & integral h = - (integral f) )
let A be closed-interval Subset of REAL ; :: thesis: for f, h being Function of A,the carrier of X st h = - f & f is integrable holds
( h is integrable & integral h = - (integral f) )
let f, h be Function of A,the carrier of X; :: thesis: ( h = - f & f is integrable implies ( h is integrable & integral h = - (integral f) ) )
assume AS: ( h = - f & f is integrable ) ; :: thesis: ( h is integrable & integral h = - (integral f) )
then A1: h = (- 1) (#) f by VFUNCT_1:29;
hence h is integrable by AS, LMth03; :: thesis: integral h = - (integral f)
integral h = (- 1) * (integral f) by AS, A1, LMth03;
hence integral h = - (integral f) by RLVECT_1:29; :: thesis: verum