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