deffunc H₁( Real) -> Element of REAL = $1 #Z q;
consider f being Function of REAL ,REAL such that
A1: for d being Element of REAL holds f . d = H₁(d) from FUNCT_2:sch 4();
take f ; :: thesis: for x being real number holds f . x = x #Z q
let d be real number ; :: thesis: f . d = d #Z q
d is Real by XREAL_0:def 1;
hence f . d = d #Z q by A1; :: thesis: verum