let x be Element of REAL ; :: thesis: sin_C /. x = sin . x
x in REAL ;
then reconsider z = x as Element of COMPLEX by NUMBERS:11;
sin_C /. x = sin_C /. z
.= ((exp ((- 0 ) + (x * <i> ))) - (exp (- (<i> * x)))) / (2 * <i> ) by Def1
.= ((((exp_R . 0 ) * (cos . x)) + (((exp_R . 0 ) * (sin . x)) * <i> )) - (exp (- (x * <i> )))) / (2 * <i> ) by Th19
.= ((((exp_R 0 ) * (cos . x)) + (((exp_R . 0 ) * (sin . x)) * <i> )) - (exp (- (x * <i> )))) / (2 * <i> ) by SIN_COS:def 27
.= ((((exp_R 0 ) * (cos . x)) + (((exp_R 0 ) * (sin . x)) * <i> )) - (exp (- (x * <i> )))) / (2 * <i> ) by SIN_COS:def 27
.= (((cos . x) + ((sin . x) * <i> )) - (exp (0 + ((- x) * <i> )))) / (2 * <i> ) by SIN_COS:56
.= (((cos . x) + ((sin . x) * <i> )) - (((exp_R . 0 ) * (cos . (- x))) + (((exp_R . 0 ) * (sin . (- x))) * <i> ))) / (2 * <i> ) by Th19
.= (((cos . x) + ((sin . x) * <i> )) - (((exp_R 0 ) * (cos . (- x))) + (((exp_R . 0 ) * (sin . (- x))) * <i> ))) / (2 * <i> ) by SIN_COS:def 27
.= (((cos . x) + ((sin . x) * <i> )) - ((1 * (cos . (- x))) + ((1 * (sin . (- x))) * <i> ))) / (2 * <i> ) by SIN_COS:56, SIN_COS:def 27
.= (((cos . x) + ((sin . x) * <i> )) - ((cos . (- x)) + ((- (sin . x)) * <i> ))) / (2 * <i> ) by SIN_COS:33
.= (((cos . x) + ((sin . x) * <i> )) - ((cos . x) + ((- (sin . x)) * <i> ))) / (2 * <i> ) by SIN_COS:33
.= sin . x ;
hence sin_C /. x = sin . x ; :: thesis: verum