cos . (- (PI / 2)) = cos . ((- (PI / 2)) + (2 * PI)) by SIN_COS:78
.= 0 by SIN_COS:76 ;
hence ( cos (- (PI / 2)) = 0 & cos . (- (PI / 2)) = 0 ) by SIN_COS:def 19; :: thesis: verum