let A be closed-interval Subset of REAL ; :: thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
( f - g is integrable & integral (f - g) = (integral f) - (integral g) )
let f, g be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable implies ( f - g is integrable & integral (f - g) = (integral f) - (integral g) ) )
assume A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable ) ; :: thesis: ( f - g is integrable & integral (f - g) = (integral f) - (integral g) )
then A2: (- g) | A is bounded by RFUNCT_1:99;
- g = (- 1) (#) g ;
then A3: ( - g is integrable & integral (- g) = (- 1) * (integral g) ) by A1, Th31;
hence f - g is integrable by A1, A2, INTEGRA1:59; :: thesis: integral (f - g) = (integral f) - (integral g)
integral (f - g) = (integral f) + (- (integral g)) by A1, A2, A3, INTEGRA1:59;
hence integral (f - g) = (integral f) - (integral g) ; :: thesis: verum