let x be Real; :: thesis: sin_C /. x = sin . x
x in REAL by XREAL_0:def 1;
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 23
.= ((((exp_R 0) * (cos . x)) + (((exp_R 0) * (sin . x)) * <i>)) - (exp (- (x * <i>)))) / (2 * <i>) by SIN_COS:def 23
.= (((cos . x) + ((sin . x) * <i>)) - (exp (0 + ((- x) * <i>)))) / (2 * <i>) by SIN_COS:51
.= (((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 23
.= (((cos . x) + ((sin . x) * <i>)) - ((1 * (cos . (- x))) + ((1 * (sin . (- x))) * <i>))) / (2 * <i>) by SIN_COS:51, SIN_COS:def 23
.= (((cos . x) + ((sin . x) * <i>)) - ((cos . (- x)) + ((- (sin . x)) * <i>))) / (2 * <i>) by SIN_COS:30
.= (((cos . x) + ((sin . x) * <i>)) - ((cos . x) + ((- (sin . x)) * <i>))) / (2 * <i>) by SIN_COS:30
.= sin . x ;
hence sin_C /. x = sin . x ; :: thesis: verum