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 = [.a,b.] 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 = [.a,b.] holds

integral (f,A) = integral (f,a,b)

let a, b be Real; :: thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) )

assume A1: A = [.a,b.] ; :: thesis: integral (f,A) = integral (f,a,b)

( Re (integral (f,A)) = integral ((Re f),A) & Im (integral (f,A)) = integral ((Im f),A) & Re (integral (f,a,b)) = integral ((Re f),a,b) & Im (integral (f,a,b)) = integral ((Im f),a,b) ) by COMPLEX1:12;

then ( Re (integral (f,A)) = Re (integral (f,a,b)) & Im (integral (f,A)) = Im (integral (f,a,b)) ) by A1, INTEGRA5:19;

hence integral (f,A) = integral (f,a,b) ; :: thesis: verum

for a, b being Real st A = [.a,b.] 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 = [.a,b.] holds

integral (f,A) = integral (f,a,b)

let a, b be Real; :: thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) )

assume A1: A = [.a,b.] ; :: thesis: integral (f,A) = integral (f,a,b)

( Re (integral (f,A)) = integral ((Re f),A) & Im (integral (f,A)) = integral ((Im f),A) & Re (integral (f,a,b)) = integral ((Re f),a,b) & Im (integral (f,a,b)) = integral ((Im f),a,b) ) by COMPLEX1:12;

then ( Re (integral (f,A)) = Re (integral (f,a,b)) & Im (integral (f,A)) = Im (integral (f,a,b)) ) by A1, INTEGRA5:19;

hence integral (f,A) = integral (f,a,b) ; :: thesis: verum