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