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