:: deftheorem Def4 defines integral INTEGR1C:def 4 :
for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f holds
for b₃ being Complex holds
( b₃ = integral (f,C) iff ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b₃ = integral (f,x,y,a,b,Z) ) );