let f be PartFunc of REAL,COMPLEX; 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; for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
let a, b be Real; ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) )
assume A1:
A = [.b,a.]
; - (integral (f,A)) = integral (f,a,b)
A2:
( Re (integral (f,a,b)) = integral ((Re f),a,b) & Im (integral (f,a,b)) = integral ((Im f),a,b) )
by COMPLEX1:12;
A3: Re (- (integral (f,A))) =
- (Re (integral (f,A)))
by COMPLEX1:17
.=
- (integral ((Re f),A))
by COMPLEX1:12
;
A4: Im (- (integral (f,A))) =
- (Im (integral (f,A)))
by COMPLEX1:17
.=
- (integral ((Im f),A))
by COMPLEX1:12
;
A5:
Re (- (integral (f,A))) = Re (integral (f,a,b))
by A3, A1, A2, INTEGRA5:20;
Im (- (integral (f,A))) = Im (integral (f,a,b))
by A4, A1, A2, INTEGRA5:20;
hence
- (integral (f,A)) = integral (f,a,b)
by A5; verum