deffunc H1( object ) -> Element of the carrier of (TOP-REAL 1) = |[(f . $1)]|;
ex F being Function st
( dom F = dom f & ( for x being object st x in dom f holds
F . x = H1(x) ) )
from FUNCT_1:sch 3();
hence
ex b1 being Function st
( dom b1 = dom f & ( for x being object st x in dom b1 holds
b1 . x = |[(f . x)]| ) )
; verum