let f be PartFunc of REAL,COMPLEX; :: 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: ( 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; :: thesis: verum

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: ( 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; :: thesis: verum