deffunc H₁( Element of COMPLEX ) -> Element of COMPLEX = ((exp (<i> * $1)) + (exp (- (<i> * $1)))) / 2;
ex f being Function of COMPLEX ,COMPLEX st
for z being Element of COMPLEX holds f . z = H₁(z) from FUNCT_2:sch 4();
hence ex b₁ being Function of COMPLEX ,COMPLEX st
for z being Element of COMPLEX holds b₁ . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ; :: thesis: verum