let th be real number ; :: 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:79
.= ((sin . th) * (cos . PI )) + ((cos . th) * (sin . (- PI ))) by SIN_COS:33
.= ((sin . th) * (cos . PI )) + ((cos . th) * (- (sin . PI ))) by SIN_COS:33
.= - (sin . th) by SIN_COS:81 ; :: thesis: cos . (th - PI ) = - (cos . th)
thus cos . (th - PI ) = ((cos . th) * (cos . (- PI ))) - ((sin . th) * (sin . (- PI ))) by SIN_COS:79
.= ((cos . th) * (cos . PI )) - ((sin . th) * (sin . (- PI ))) by SIN_COS:33
.= ((cos . th) * (cos . PI )) - ((sin . th) * (- (sin . PI ))) by SIN_COS:33
.= - (cos . th) by SIN_COS:81 ; :: thesis: verum