let X be RealNormSpace; :: thesis: for A being closed-interval Subset of REAL
for f, g, h being Function of A,the carrier of X st h = f - g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) - (integral g) )
let A be closed-interval Subset of REAL ; :: thesis: for f, g, h being Function of A,the carrier of X st h = f - g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) - (integral g) )
let f, g, h be Function of A,the carrier of X; :: thesis: ( h = f - g & f is integrable & g is integrable implies ( h is integrable & integral h = (integral f) - (integral g) ) )
assume AS: ( h = f - g & f is integrable & g is integrable ) ; :: thesis: ( h is integrable & integral h = (integral f) - (integral g) )
then A1: h = f + (- g) by VFUNCT_1:31;
dom (- g) = dom g by VFUNCT_1:def 6
.= A by FUNCT_2:def 1 ;
then reconsider gg = - g as Function of A,the carrier of X by FUNCT_2:def 1;
A2: gg is integrable by AS, LMth03a;
hence h is integrable by AS, A1, LMth01; :: thesis: integral h = (integral f) - (integral g)
integral h = (integral f) + (integral gg) by AS, A1, A2, LMth01;
then integral h = (integral f) + (- (integral g)) by AS, LMth03a;
hence integral h = (integral f) - (integral g) by RLVECT_1:def 14; :: thesis: verum