let X be RealNormSpace; for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let A be non empty closed_interval Subset of REAL; for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let f1, f2 be PartFunc of REAL, the carrier of X; ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 implies ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) )
assume that
A1:
( f1 is_integrable_on A & f2 is_integrable_on A )
and
A2:
( A c= dom f1 & A c= dom f2 )
; ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
A3:
f1 - f2 = f1 + (- f2)
by VFUNCT_1:25;
A4:
dom (- f2) = dom f2
by VFUNCT_1:def 5;
A5:
- f2 = (- jj) (#) f2
by VFUNCT_1:23;
then A6:
- f2 is_integrable_on A
by A1, A2, Th13;
hence
f1 - f2 is_integrable_on A
by A1, A2, A3, A4, Th14; integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A))
thus integral ((f1 - f2),A) =
integral ((f1 + (- f2)),A)
by VFUNCT_1:25
.=
(integral (f1,A)) + (integral ((- f2),A))
by A1, A2, A4, A6, Th14
.=
(integral (f1,A)) + ((- jj) * (integral (f2,A)))
by A1, A2, A5, Th13
.=
(integral (f1,A)) + (- (integral (f2,A)))
by RLVECT_1:16
.=
(integral (f1,A)) - (integral (f2,A))
by RLVECT_1:def 11
; verum