let x be Real; :: thesis: cos_C /. x = cos . x
x in REAL by XREAL_0:def 1;
then reconsider z = x as Element of COMPLEX by NUMBERS:11;
cos_C /. x = cos_C /. z
.= ((exp (0 + (<i> * x))) + (exp (- (<i> * x)))) / 2 by Def2
.= ((((exp_R . 0) * (cos . x)) + (((exp_R . 0) * (sin . x)) * <i>)) + (exp (- (<i> * x)))) / 2 by Th19
.= ((((exp_R 0) * (cos . x)) + (((exp_R . 0) * (sin . x)) * <i>)) + (exp (- (<i> * x)))) / 2 by SIN_COS:def 23
.= (((1 * (cos . x)) + ((1 * (sin . x)) * <i>)) + (exp (- (<i> * x)))) / 2 by SIN_COS:51, SIN_COS:def 23
.= (((cos . x) + ((sin . x) * <i>)) + (exp (0 + ((- x) * <i>)))) / 2
.= (((cos . x) + ((sin . x) * <i>)) + (((exp_R . 0) * (cos . (- x))) + (((exp_R . 0) * (sin . (- x))) * <i>))) / 2 by Th19
.= (((cos . x) + ((sin . x) * <i>)) + (((exp_R 0) * (cos . (- x))) + (((exp_R . 0) * (sin . (- x))) * <i>))) / 2 by SIN_COS:def 23
.= (((cos . x) + ((sin . x) * <i>)) + ((1 * (cos . (- x))) + ((1 * (sin . (- x))) * <i>))) / 2 by SIN_COS:51, SIN_COS:def 23
.= (((cos . x) + ((sin . x) * <i>)) + ((1 * (cos . x)) + ((1 * (sin . (- x))) * <i>))) / 2 by SIN_COS:30
.= (((cos . x) + ((sin . x) * <i>)) + ((cos . x) + ((- (sin . x)) * <i>))) / 2 by SIN_COS:30
.= cos . x ;
hence cos_C /. x = cos . x ; :: thesis: verum