deffunc H₁( Real) -> Element of REAL = In ((((exp_R . $1) + (exp_R . (- $1))) / 2),REAL);
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 d being Real holds f . d = ((exp_R . d) + (exp_R . (- d))) / 2
let d be Real; :: thesis: f . d = ((exp_R . d) + (exp_R . (- d))) / 2
d in REAL by XREAL_0:def 1;
then f . d = H₁(d) by A1;
hence f . d = ((exp_R . d) + (exp_R . (- d))) / 2 ; :: thesis: verum