sinh_C /. 0c = ((exp 0c) - (exp (- 0c))) / 2 by Def3
.= 0c / 2 ;
hence sinh_C /. 0c = 0 ; :: thesis: verum