deffunc H₁( 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₁(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₁(x) by A1;
hence f . x = sgn x ; :: thesis: verum