let z1, z2 be Element of COMPLEX ; :: thesis: cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2))
cos_C /. (z1 - z2) = cos_C /. (z1 + (- z2))
.= ((cos_C /. z1) * (cos_C /. (- z2))) - ((sin_C /. z1) * (sin_C /. (- z2))) by Th6
.= ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. (- z2))) by Th3
.= ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (- (sin_C /. z2))) by Th2
.= ((cos_C /. z1) * (cos_C /. z2)) - (- ((sin_C /. z1) * (sin_C /. z2))) ;
hence cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2)) ; :: thesis: verum