A1: sin . (- (PI / 4)) = - (1 / (sqrt 2)) by Th29, SIN_COS:33;
A2: cos . (- (PI / 4)) = 1 / (sqrt 2) by Th29, SIN_COS:33;
A3: sin . ((3 / 4) * PI ) = sin . (PI + (- (PI / 4)))
.= - (- (1 / (sqrt 2))) by A1, SIN_COS:83
.= 1 / (sqrt 2) ;
cos . ((3 / 4) * PI ) = cos . (PI + (- (PI / 4)))
.= - (1 / (sqrt 2)) by A2, SIN_COS:83 ;
hence ( sin . (- (PI / 4)) = - (1 / (sqrt 2)) & cos . (- (PI / 4)) = 1 / (sqrt 2) & sin . ((3 / 4) * PI ) = 1 / (sqrt 2) & cos . ((3 / 4) * PI ) = - (1 / (sqrt 2)) ) by A3, Th29, SIN_COS:33; :: thesis: verum