:: deftheorem defines is_integrable_on INTEGR16:def 7 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX holds
( f is_integrable_on A iff ( Re f is_integrable_on A & Im f is_integrable_on A ) );