theorem Th6: :: SIN_COS3:6

for z1, z2 being Complex holds cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))