let x, y, z be Real; :: thesis: ( (x - ((- (2 * PI)) + y)) + z = PI implies (((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2 )
assume (x - ((- (2 * PI)) + y)) + z = PI ; :: thesis: (((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2
then A1: (x + (- ((- (2 * PI)) + y))) + z = PI ;
(((sin x) ^2) + ((sin (- ((- (2 * PI)) + y))) ^2)) - (((2 * (sin x)) * (sin (- ((- (2 * PI)) + y)))) * (cos z)) = (((sin x) ^2) + ((sin (- ((- (2 * PI)) + y))) ^2)) - (((2 * (sin x)) * (- (sin ((- (2 * PI)) + y)))) * (cos z)) by SIN_COS:31
.= (((sin x) ^2) + ((sin (- ((- (2 * PI)) + y))) ^2)) + (((2 * (sin x)) * (sin ((- (2 * PI)) + y))) * (cos z))
.= (((sin x) ^2) + ((sin ((- (2 * PI)) + y)) ^2)) + (((2 * (sin x)) * (sin ((- (2 * PI)) + y))) * (cos z)) by Thm16
.= (((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin ((- (2 * PI)) + y))) * (cos z)) by Thm2
.= (((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) by Thm2 ;
hence (((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2 by A1, Thm17; :: thesis: verum