let x be Element of REAL ; :: thesis: cos_C /. x = cos . x
x in REAL ;
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 27
.= (((1 * (cos . x)) + ((1 * (sin . x)) * <i> )) + (exp (- (<i> * x)))) / 2 by SIN_COS:56, SIN_COS:def 27
.= (((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 27
.= (((cos . x) + ((sin . x) * <i> )) + ((1 * (cos . (- x))) + ((1 * (sin . (- x))) * <i> ))) / 2 by SIN_COS:56, SIN_COS:def 27
.= (((cos . x) + ((sin . x) * <i> )) + ((1 * (cos . x)) + ((1 * (sin . (- x))) * <i> ))) / 2 by SIN_COS:33
.= (((cos . x) + ((sin . x) * <i> )) + ((cos . x) + ((- (sin . x)) * <i> ))) / 2 by SIN_COS:33
.= cos . x ;
hence cos_C /. x = cos . x ; :: thesis: verum