let f be UnOp of [.0,1.]; :: thesis: ( f is REAL -defined & f is real-valued )
dom f = [.0,1.] by FUNCT_2:def 1;
hence ( f is REAL -defined & f is real-valued ) by RELAT_1:def 18; :: thesis: verum