:: deftheorem defines integrable INTEGR16:def 5 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX holds
( f is integrable iff ( Re f is integrable & Im f is integrable ) );