Loading [MathJax]/extensions/tex2jax.js
begin
Lm1:
for z being complex number holds sinh_C /. z = ((exp z) - (exp (- z))) / 2
Lm2:
for z being complex number holds cosh_C /. z = ((exp z) + (exp (- z))) / 2
Lm3:
for z being Element of COMPLEX holds (exp z) * (exp (- z)) = 1
begin
Lm4:
for x, y being Element of REAL holds exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>))
Lm5:
for z1 being Element of COMPLEX holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1