let f be PartFunc of REAL ,COMPLEX ; :: thesis: for A being 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 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:28;
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 by COMPLEX1:def 5; :: thesis: verum