let X be RealNormSpace; :: thesis: for A being non empty 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 non empty 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 A1: ( h = f - g & f is integrable & g is integrable ) ; :: thesis: ( h is integrable & integral h = (integral f) - (integral g) )
then A2: h = f + (- g) by VFUNCT_1:25;
dom (- g) = dom g by VFUNCT_1:def 5
.= A by FUNCT_2:def 1 ;
then reconsider gg = - g as Function of A, the carrier of X by FUNCT_2:def 1;
A3: gg is integrable by A1, Th5;
hence h is integrable by A1, A2, Th6; :: thesis: integral h = (integral f) - (integral g)
integral h = (integral f) + (integral gg) by A1, A2, A3, Th6;
then integral h = (integral f) + (- (integral g)) by A1, Th5;
hence integral h = (integral f) - (integral g) by RLVECT_1:def 11; :: thesis: verum