let X be RealNormSpace; :: thesis: for A being 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 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)) )
Q1: f1 - f2 = f1 + (- f2) by VFUNCT_1:31;
Q2: dom (- f2) = dom f2 by VFUNCT_1:def 6;
Q3: - f2 = (- 1) (#) f2 by VFUNCT_1:29;
then Q4: - f2 is_integrable_on A by A1, A2, th001;
hence f1 - f2 is_integrable_on A by A1, A2, Q1, Q2, th002; :: thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A))
thus integral ((f1 - f2),A) = integral ((f1 + (- f2)),A) by VFUNCT_1:31
.= (integral (f1,A)) + (integral ((- f2),A)) by A1, A2, Q2, Q4, th002
.= (integral (f1,A)) + ((- 1) * (integral (f2,A))) by A1, A2, Q3, th001
.= (integral (f1,A)) + (- (integral (f2,A))) by RLVECT_1:29
.= (integral (f1,A)) - (integral (f2,A)) by RLVECT_1:def 14 ; :: thesis: verum