let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,COMPLEX holds
( f is bounded iff ( Re f is bounded & Im f is bounded ) )
let f be Function of A,COMPLEX; :: thesis: ( f is bounded iff ( Re f is bounded & Im f is bounded ) )
dom f = A by FUNCT_2:def 1;
then reconsider f0 = f as PartFunc of REAL,COMPLEX by RELSET_1:5;
( f0 is bounded iff ( Re f0 is bounded & Im f0 is bounded ) ) by Th11;
hence ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) ; :: thesis: verum