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