deffunc H1( Real) -> set = (h ") . (f . (h . $1));
A1: for a being Element of [.0,1.] holds H1(a) in [.0,1.]
proof
let a be Element of [.0,1.]; :: thesis: H1(a) in [.0,1.]
(h ") . (f . (h . a)) in [.0,1.] ;
hence H1(a) in [.0,1.] ; :: thesis: verum
end;
ex f being UnOp of [.0,1.] st
for a being Element of [.0,1.] holds f . a = H1(a) from FUNCT_2:sch 8(A1);
 hence ex b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b1 . x = (h ") . (f . (h . x)) ; :: thesis: verum