deffunc H₁( Element of INT.Ring) -> set = absreal . $1;
thus for f1, f2 being Function of INT.Ring,NAT st ( for x being Element of INT.Ring holds f1 . x = H₁(x) ) & ( for x being Element of INT.Ring holds f2 . x = H₁(x) ) holds
f1 = f2 from BINOP_2:sch 1(); :: thesis: verum