set c = the carrier of T;
reconsider f = the carrier of T --> (In (0,REAL)) as RealMap of T ;
take f ; :: thesis: f is bounded
( dom f = the carrier of T & rng f = {0} ) by FUNCOP_1:8, FUNCT_2:def 1;
hence f .: the carrier of T is bounded_above by RELAT_1:113; :: according to SEQ_2:def 8,MEASURE6:def 11 :: thesis: f is bounded_below
thus f .: the carrier of T is bounded_below ; :: according to MEASURE6:def 10 :: thesis: verum