deffunc H₁( set ) -> set = (f . $1) " ;
ex h being Function st
( dom h = (dom f) \ (f " {0 }) & ( for x being set st x in (dom f) \ (f " {0 }) holds
h . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = (dom f) \ (f " {0 }) & ( for c being set st c in dom b₁ holds
b₁ . c = (f . c) " ) ) ; :: thesis: verum