deffunc H_{1}( Real) -> Element of REAL = In (($1 #Z q),REAL);

consider f being Function of REAL,REAL such that

A1: for d being Element of REAL holds f . d = H_{1}(d)
from FUNCT_2:sch 4();

take f ; :: thesis: for x being Real holds f . x = x #Z q

let d be Real; :: thesis: f . d = d #Z q

d in REAL by XREAL_0:def 1;

then f . d = H_{1}(d)
by A1;

hence f . d = d #Z q ; :: thesis: verum

consider f being Function of REAL,REAL such that

A1: for d being Element of REAL holds f . d = H

take f ; :: thesis: for x being Real holds f . x = x #Z q

let d be Real; :: thesis: f . d = d #Z q

d in REAL by XREAL_0:def 1;

then f . d = H

hence f . d = d #Z q ; :: thesis: verum