deffunc H₁( set ) -> set = Funcs ((f . $1),X);
ex F being Function st
( dom F = dom f & ( for x being set st x in dom f holds
F . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = dom f & ( for x being set st x in dom f holds
b₁ . x = Funcs ((f . x),X) ) ) ; :: thesis: verum