let X be RealNormSpace; :: thesis: for A being non empty 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 non empty 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 A1: ( h = - f & f is integrable ) ; :: thesis: ( h is integrable & integral h = - (integral f) )
then A2: h = (- jj) (#) f by VFUNCT_1:23;
hence h is integrable by A1, Th4; :: thesis: integral h = - (integral f)
integral h = (- jj) * (integral f) by A1, A2, Th4;
hence integral h = - (integral f) by RLVECT_1:16; :: thesis: verum