deffunc H₁( Element of REAL ) -> Element of REAL = sgn $1;
consider f being Function of REAL,REAL such that
A1: for x being Real holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being Real holds f . x = sgn x
thus for x being Real holds f . x = sgn x by A1; :: thesis: verum