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