let x be Real; :: thesis: (sin (- x)) ^2 = (sin x) ^2
(sin (- x)) ^2 = (sin (- x)) * (sin (- x)) by SQUARE_1:def 1
.= (- (sin x)) * (sin (- x)) by SIN_COS:31
.= (- (sin x)) * (- (sin x)) by SIN_COS:31
.= (sin x) * (sin x) ;
hence (sin (- x)) ^2 = (sin x) ^2 by SQUARE_1:def 1; :: thesis: verum