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

( 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