let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)

for A being non empty 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 non empty 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 non empty 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 A1: A = [.b,a.] ; :: thesis: - (integral (f,A)) = integral (f,a,b)

dom (- (integral (f,A))) = dom ((- jj) (#) (integral (f,A))) by VALUED_1:def 6

.= dom (integral (f,A)) by VALUED_1:def 5

.= Seg n by Def17

.= dom (integral (f,a,b)) by Def18 ;

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

for A being non empty 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 non empty 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 non empty 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 A1: A = [.b,a.] ; :: thesis: - (integral (f,A)) = integral (f,a,b)

A2: now :: thesis: for i being Nat st i in dom (- (integral (f,A))) holds

(- (integral (f,A))) . i = (integral (f,a,b)) . i

reconsider jj = 1 as Real ;(- (integral (f,A))) . i = (integral (f,a,b)) . i

let i be Nat; :: thesis: ( i in dom (- (integral (f,A))) implies (- (integral (f,A))) . i = (integral (f,a,b)) . i )

assume A3: i in dom (- (integral (f,A))) ; :: thesis: (- (integral (f,A))) . i = (integral (f,a,b)) . i

then reconsider k = i as Element of NAT ;

A4: dom (integral (f,A)) = Seg n by Def17;

A5: k in dom (integral (f,A)) by A3, VALUED_1:8;

then A6: (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) by A4, Def18;

(- (integral (f,A))) . k = - ((integral (f,A)) . k) by VALUED_1:8

.= - (integral (((proj (k,n)) * f),A)) by A5, A4, Def17 ;

hence (- (integral (f,A))) . i = (integral (f,a,b)) . i by A1, A6, INTEGRA5:20; :: thesis: verum

end;assume A3: i in dom (- (integral (f,A))) ; :: thesis: (- (integral (f,A))) . i = (integral (f,a,b)) . i

then reconsider k = i as Element of NAT ;

A4: dom (integral (f,A)) = Seg n by Def17;

A5: k in dom (integral (f,A)) by A3, VALUED_1:8;

then A6: (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) by A4, Def18;

(- (integral (f,A))) . k = - ((integral (f,A)) . k) by VALUED_1:8

.= - (integral (((proj (k,n)) * f),A)) by A5, A4, Def17 ;

hence (- (integral (f,A))) . i = (integral (f,a,b)) . i by A1, A6, INTEGRA5:20; :: thesis: verum

dom (- (integral (f,A))) = dom ((- jj) (#) (integral (f,A))) by VALUED_1:def 6

.= dom (integral (f,A)) by VALUED_1:def 5

.= Seg n by Def17

.= dom (integral (f,a,b)) by Def18 ;

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