deffunc H₁( Complex) -> Element of COMPLEX = In ((((exp (<i> * $1)) + (exp (- (<i> * $1)))) / 2),COMPLEX);
consider f being Function of COMPLEX,COMPLEX such that
A1: for z being Element of COMPLEX holds f . z = H₁(z) from FUNCT_2:sch 4();
take f ; :: thesis: for z being Complex holds f . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2
let z be Complex; :: thesis: f . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
f . z = H₁(z) by A1;
hence f . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ; :: thesis: verum