cosh_C /. 0c = ((exp 0c) + (exp (- 0c))) / 2 by Def4
.= 1 by SIN_COS:49, SIN_COS:51 ;
hence cosh_C /. 0c = 1 ; :: thesis: verum