deffunc H₁( object ) -> set = Funcs ((f . $1),X);
consider F being Function such that
A1: ( dom F = dom f & ( for x being object st x in dom f holds
F . x = H₁(x) ) ) from FUNCT_1:sch 3();
take F ; :: thesis: ( dom F = dom f & ( for x being object st x in dom f holds
F . x = Funcs ((f . x),X) ) )
thus ( dom F = dom f & ( for x being object st x in dom f holds
F . x = Funcs ((f . x),X) ) ) by A1; :: thesis: verum