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

consider f being Function of REAL,REAL such that

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

take f ; :: thesis: for x being Real holds f . x = sgn x

let x be Real; :: thesis: f . x = sgn x

x in REAL by XREAL_0:def 1;

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

hence f . x = sgn x ; :: thesis: verum

consider f being Function of REAL,REAL such that

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

take f ; :: thesis: for x being Real holds f . x = sgn x

let x be Real; :: thesis: f . x = sgn x

x in REAL by XREAL_0:def 1;

then f . x = H

hence f . x = sgn x ; :: thesis: verum