let z be Element of COMPLEX ; :: thesis: ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1
set z1 = exp (<i> * z);
set z2 = exp (- (<i> * z));
((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2)) by Def2
.= ((sin_C /. z) * (sin_C /. z)) + ((((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) * (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2)) by Def2
.= ((((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>)) * (sin_C /. z)) + ((((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) * (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2)) by Def1
.= ((((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>)) * (((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>))) + ((((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) * (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2)) by Def1
.= ((((exp (<i> * z)) * (exp (- (<i> * z)))) + ((exp (<i> * z)) * (exp (- (<i> * z))))) + (((exp (<i> * z)) * (exp (- (<i> * z)))) + ((exp (<i> * z)) * (exp (- (<i> * z)))))) / 4
.= ((1 + ((exp (<i> * z)) * (exp (- (<i> * z))))) + (((exp (<i> * z)) * (exp (- (<i> * z)))) + ((exp (<i> * z)) * (exp (- (<i> * z)))))) / 4 by Lm3
.= ((1 + 1) + (((exp (<i> * z)) * (exp (- (<i> * z)))) + ((exp (<i> * z)) * (exp (- (<i> * z)))))) / 4 by Lm3
.= ((1 + 1) + (((exp (<i> * z)) * (exp (- (<i> * z)))) + 1)) / 4 by Lm3
.= (2 + 2) / 4 by Lm3 ;
hence ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1 ; :: thesis: verum