let n be Element of NAT ; :: thesis: for f being PartFunc of REAL ,(REAL n)
for A being closed-interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral f,A) = integral f,a,b
let f be PartFunc of REAL ,(REAL n); :: thesis: for A being closed-interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral f,A) = integral f,a,b
let A be closed-interval Subset of REAL ; :: thesis: for a, b being Real st A = [.b,a.] holds
- (integral f,A) = integral f,a,b
let a, b be Real; :: thesis: ( A = [.b,a.] implies - (integral f,A) = integral f,a,b )
assume A0: A = [.b,a.] ; :: thesis: - (integral f,A) = integral f,a,b
A1: dom (- (integral f,A)) = dom ((- 1) (#) (integral f,A)) by VALUED_1:def 6
.= dom (integral f,A) by VALUED_1:def 5
.= Seg n by DefintN
.= dom (integral f,a,b) by Defintn ;

now

let i be Nat; :: thesis: ( i in dom (- (integral f,A)) implies (- (integral f,A)) . i = (integral f,a,b) . i )
assume B1: i in dom (- (integral f,A)) ; :: thesis: (- (integral f,A)) . i = (integral f,a,b) . i
then reconsider k = i as Element of NAT ;
B2: k in dom (integral f,A) by B1, VALUED_1:8;
B3: dom (integral f,A) = Seg n by DefintN;
B4: (- (integral f,A)) . k = - ((integral f,A) . k) by VALUED_1:8
.= - (integral ((proj k,n) * f),A) by B2, B3, DefintN ;
(integral f,a,b) . k = integral ((proj k,n) * f),a,b by B2, B3, Defintn;
hence (- (integral f,A)) . i = (integral f,a,b) . i by A0, B4, INTEGRA5:20; :: thesis: verum

end;

hence - (integral f,A) = integral f,a,b by A1, FINSEQ_1:17; :: thesis: verum