sinh . 0 = ((exp_R . 0) - (exp_R . (- 0))) / 2 by Def1
.= 0 ;
hence sinh . 0 = 0 ; :: thesis: verum