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