for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX holds
( f is bounded iff ( Re f is bounded & Im f is bounded ) )