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