:: deftheorem defines integral INTEGR16:def 9 :
for a, b being Real
for f being PartFunc of REAL,COMPLEX holds integral (f,a,b) = (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>);