let f be bijective UnOp of [.0,1.]; :: thesis: (f | [.0,1.]) " is REAL -defined
dom (f ") = rng f by FUNCT_1:33;
hence (f | [.0,1.]) " is REAL -defined by RELAT_1:def 18, RELAT_1:def 19; :: thesis: verum