for z being Element of COMPLEX holds ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1