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