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