cos . (- (PI / 2)) = cos . ((- (PI / 2)) + (2 * PI )) by SIN_COS:83
.= 0 by SIN_COS:81 ;
hence ( cos (- (PI / 2)) = 0 & cos . (- (PI / 2)) = 0 ) by SIN_COS:def 23; :: thesis: verum