sin . (- (PI / 2)) = sin . ((- (PI / 2)) + (2 * PI )) by SIN_COS:83
.= - 1 by SIN_COS:81 ;
hence ( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 ) by SIN_COS:def 21; :: thesis: verum