deffunc H₁( object ) -> object = (f . $1) mod m;
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 i being object st i in dom f holds
g . i = (f . i) mod m ) )
thus ( dom g = dom f & ( for i being object st i in dom f holds
g . i = (f . i) mod m ) ) by A1, A2; :: thesis: verum