let X be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: verum