deffunc H_{1}( 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_{1}(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

consider h being Function such that

A1: ( dom h = dom f & ( for x being object st x in dom f holds

h . x = H

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