let f be PartFunc of REAL ,COMPLEX ; :: 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 A1: A = [.b,a.] ; :: thesis: - (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:28;
X1: Re (- (integral f,A)) = - (Re (integral f,A)) by COMPLEX1:34
.= - (integral (Re f),A) by COMPLEX1:28 ;
X2: Im (- (integral f,A)) = - (Im (integral f,A)) by COMPLEX1:34
.= - (integral (Im f),A) by COMPLEX1:28 ;
Y1: Re (- (integral f,A)) = Re (integral f,a,b) by X1, A1, A2, INTEGRA5:20;
Im (- (integral f,A)) = Im (integral f,a,b) by X2, A1, A2, INTEGRA5:20;
hence - (integral f,A) = integral f,a,b by COMPLEX1:def 5, Y1; :: thesis: verum