deffunc H₁( Element of COMPLEX ) -> Element of COMPLEX = ((exp $1) - (exp (- $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 z) - (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b₂ . z = ((exp z) - (exp (- z))) / 2 ) holds
b₁ = b₂ ; :: thesis: verum