let A be non empty 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 that
A1: ( f | A is bounded & f is integrable ) and
A2: g | A is bounded and
A3: g is integrable ; :: thesis: ( f - g is integrable & integral (f - g) = (integral f) - (integral g) )
A4: - g is integrable by A2, A3, Th31;
A5: (- g) | A is bounded by A2, RFUNCT_1:82;
hence f - g is integrable by A1, A4, INTEGRA1:57; :: thesis: integral (f - g) = (integral f) - (integral g)
integral (- g) = (- 1) * (integral g) by A2, A3, Th31;
then integral (f - g) = (integral f) + (- (integral g)) by A1, A5, A4, INTEGRA1:57;
hence integral (f - g) = (integral f) - (integral g) ; :: thesis: verum