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