let f be one-to-one UnOp of [.0,1.]; :: thesis: for d being Element of [.0,1.] st d in rng f holds
(f ") . d in dom f
let d be Element of [.0,1.]; :: thesis: ( d in rng f implies (f ") . d in dom f )
set X = [.0,1.];
reconsider fX = f | [.0,1.] as PartFunc of [.0,1.],[.0,1.] ;
assume a1: d in rng f ; :: thesis: (f ") . d in dom f
YZ: dom f = rng (f ") by FUNCT_1:33;
reconsider dd = d as Element of REAL ;
dom (f ") = rng f by FUNCT_1:33;
hence (f ") . d in dom f by YZ, FUNCT_1:3, a1; :: thesis: verum