let z be Complex; :: thesis: ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1
set e1 = exp z;
set e2 = exp (- z);
((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = ((cosh_C /. z) * (cosh_C /. z)) - ((((exp z) - (exp (- z))) / 2) * (sinh_C /. z)) by Def3
.= ((cosh_C /. z) * (cosh_C /. z)) - ((((exp z) - (exp (- z))) / 2) * (((exp z) - (exp (- z))) / 2)) by Def3
.= ((((exp z) + (exp (- z))) / 2) * (cosh_C /. z)) - ((((exp z) - (exp (- z))) * ((exp z) - (exp (- z)))) / (2 * 2)) by Def4
.= ((((exp z) + (exp (- z))) / 2) * (((exp z) + (exp (- z))) / 2)) - ((((exp z) - (exp (- z))) * ((exp z) - (exp (- z)))) / (2 * 2)) by Def4
.= ((((exp z) * (exp (- z))) + ((exp z) * (exp (- z)))) + (((exp z) * (exp (- z))) + ((exp z) * (exp (- z))))) / (2 * 2)
.= ((1 + ((exp z) * (exp (- z)))) + (((exp z) * (exp (- z))) + ((exp z) * (exp (- z))))) / (2 * 2) by Lm3
.= ((1 + 1) + (((exp z) * (exp (- z))) + ((exp z) * (exp (- z))))) / (2 * 2) by Lm3
.= ((1 + 1) + (1 + ((exp z) * (exp (- z))))) / (2 * 2) by Lm3
.= (2 + 2) / (2 * 2) by Lm3
.= 1 ;
hence ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1 ; :: thesis: verum