let A be 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:13;
( f0 is bounded iff ( Re f0 is bounded & Im f0 is bounded ) ) by BND01A;
hence ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) ; :: thesis: verum