let z1, z2 be Complex; sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider e1 = exp (<i> * z1), e2 = exp (- (<i> * z1)), e3 = exp (<i> * z2), e4 = exp (- (<i> * z2)) as Element of COMPLEX ;
((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) =
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
by Def1
.=
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (cos_C /. z2)) + ((cos_C /. z1) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def1
.=
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (((exp (- (<i> * z2))) + (exp (<i> * z2))) / 2)) + ((cos_C /. z1) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def2
.=
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) * ((exp (- (<i> * z2))) + (exp (<i> * z2)))) / ((2 * <i>) * 2)) + ((((exp (- (<i> * z1))) + (exp (<i> * z1))) / 2) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def2
.=
(((e1 * e3) + (e1 * e3)) - (((e1 * e4) + (e2 * e4)) - ((e1 * e4) - (e2 * e4)))) / ((2 * <i>) * 2)
.=
((((Re (e1 * e3)) + (Re (e1 * e3))) + (((Im (e1 * e3)) + (Im (e1 * e3))) * <i>)) - ((e2 * e4) + (e2 * e4))) / ((2 * <i>) * 2)
by COMPLEX1:81
.=
(((2 * (Re (e1 * e3))) + ((2 * (Im (e1 * e3))) * <i>)) - ((e2 * e4) + (e2 * e4))) / ((2 * <i>) * 2)
.=
(((Re (2 * (e1 * e3))) + ((2 * (Im (e1 * e3))) * <i>)) - ((e2 * e4) + (e2 * e4))) / ((2 * <i>) * 2)
by COMSEQ_3:17
.=
(((Re (2 * (e1 * e3))) + ((Im (2 * (e1 * e3))) * <i>)) - ((e2 * e4) + (e2 * e4))) / ((2 * <i>) * 2)
by COMSEQ_3:17
.=
((2 * (e1 * e3)) - ((e2 * e4) + (e2 * e4))) / ((2 * <i>) * 2)
by COMPLEX1:13
.=
((2 * (e1 * e3)) - (((Re (e2 * e4)) + (Re (e2 * e4))) + (((Im (e2 * e4)) + (Im (e2 * e4))) * <i>))) / ((2 * <i>) * 2)
by COMPLEX1:81
.=
((2 * (e1 * e3)) - ((2 * (Re (e2 * e4))) + ((2 * (Im (e2 * e4))) * <i>))) / ((2 * <i>) * 2)
.=
((2 * (e1 * e3)) - ((Re (2 * (e2 * e4))) + ((2 * (Im (e2 * e4))) * <i>))) / ((2 * <i>) * 2)
by COMSEQ_3:17
.=
((2 * (e1 * e3)) - ((Re (2 * (e2 * e4))) + ((Im (2 * (e2 * e4))) * <i>))) / ((2 * <i>) * 2)
by COMSEQ_3:17
.=
((2 * (e1 * e3)) - (2 * (e2 * e4))) / ((2 * <i>) * 2)
by COMPLEX1:13
.=
((e1 * e3) / (2 * <i>)) - ((2 * (e2 * e4)) / ((2 * <i>) * 2))
.=
((exp ((<i> * z1) + (<i> * z2))) / (2 * <i>)) - ((e2 * e4) / (2 * <i>))
by SIN_COS:23
.=
((exp (<i> * (z1 + z2))) / (2 * <i>)) - ((exp ((- (<i> * z1)) + (- (<i> * z2)))) / (2 * <i>))
by SIN_COS:23
.=
((exp (<i> * (z1 + z2))) - (exp (- (<i> * (z1 + z2))))) / (2 * <i>)
;
then
sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
by Def1;
hence
sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
; verum