sin . (- (PI / 2)) = sin . ((- (PI / 2)) + (2 * PI)) by SIN_COS:78
.= - 1 by SIN_COS:76 ;
hence ( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 ) by SIN_COS:def 17; :: thesis: verum