let th be Real; :: thesis: ( sin . (th - PI) = - (sin . th) & cos . (th - PI) = - (cos . th) )
thus sin . (th - PI) = ((sin . th) * (cos . (- PI))) + ((cos . th) * (sin . (- PI))) by SIN_COS:74
.= ((sin . th) * (cos . PI)) + ((cos . th) * (sin . (- PI))) by SIN_COS:30
.= ((sin . th) * (cos . PI)) + ((cos . th) * (- (sin . PI))) by SIN_COS:30
.= - (sin . th) by SIN_COS:76 ; :: thesis: cos . (th - PI) = - (cos . th)
thus cos . (th - PI) = ((cos . th) * (cos . (- PI))) - ((sin . th) * (sin . (- PI))) by SIN_COS:74
.= ((cos . th) * (cos . PI)) - ((sin . th) * (sin . (- PI))) by SIN_COS:30
.= ((cos . th) * (cos . PI)) - ((sin . th) * (- (sin . PI))) by SIN_COS:30
.= - (cos . th) by SIN_COS:76 ; :: thesis: verum