sin_C /. 0c = ((exp 0c) - (exp (- (<i> * 0c)))) / (<i> * 2) by Def1
.= 0c / (<i> * 2) ;
hence sin_C /. 0c = 0 ; :: thesis: verum