let z1, z2 be Complex; :: thesis: sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2))
sin_C /. (z1 - z2) = sin_C /. (z1 + (- z2))
.= ((sin_C /. z1) * (cos_C /. (- z2))) + ((cos_C /. z1) * (sin_C /. (- z2))) by Th4
.= ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. (- z2))) by Th3
.= ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (- (sin_C /. z2))) by Th2
.= ((sin_C /. z1) * (cos_C /. z2)) + (- ((cos_C /. z1) * (sin_C /. z2))) ;
hence sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2)) ; :: thesis: verum