deffunc H₁( object ) -> object = (f . $1) `1 ;
ex g being Function st
( dom g = dom f & ( for x being object st x in dom f holds
g . x = H<sub>1</sub>(x) ) ) from FUNCT_1:sch 3();
hence ex b<sub>1</sub> being Function st
( dom b<sub>1</sub> = dom f & ( for x being object st x in dom f holds
b<sub>1</sub> . x = (f . x) `1 ) ) ; :: thesis: verum