:: deftheorem defines integral INTEGR16:def 6 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX holds integral f = (integral (Re f)) + ((integral (Im f)) * <i>);