deffunc H₁( set ) -> Real = ||.(f /. $1).||;
consider g being Function such that
W1: dom g = dom f and
W2: for x being set 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 W1, W2; :: thesis: verum