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

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