let A be non empty closed_interval Subset of REAL; 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; ( 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
; ( 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; 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)
; verum