let r be real number ; :: thesis: ( sin (r - PI ) = - (sin r) & cos (r - PI ) = - (cos r) )
thus sin (r - PI ) = ((sin r) * (cos PI )) - ((cos r) * (sin PI )) by Th4
.= - (sin r) by SIN_COS:82 ; :: thesis: cos (r - PI ) = - (cos r)
thus cos (r - PI ) = ((cos r) * (cos PI )) + ((sin r) * (sin PI )) by Th4
.= - (cos r) by SIN_COS:82 ; :: thesis: verum