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