deffunc H₁( Element of COMPLEX ) -> Element of COMPLEX = ((exp $1) + (exp (- $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 z) + (exp (- z))) / 2 ; :: thesis: verum