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

( 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