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