cosh . 0 = ((exp_R . 0) + (exp_R . (- 0))) / 2 by SIN_COS2:def 3
.= 1 by SIN_COS:51 ;
hence cosh . 0 = 1 ; :: thesis: verum