cos_C /. 0c = ((exp 0c) + (exp (- (<i> * 0c)))) / 2 by Def2
.= 1 by SIN_COS:49, SIN_COS:51 ;
hence cos_C /. 0c = 1 ; :: thesis: verum