deffunc H₁( Complex) -> Element of COMPLEX = In ((((exp (<i> * $1)) - (exp (- (<i> * $1)))) / (2 * <i>)),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 * <i>)
let z be Complex; :: thesis: f . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>)
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 * <i>) ; :: thesis: verum