let th1, th2 be Real; :: thesis: ( sin (th1 - th2) = ((sin th1) * (cos th2)) - ((cos th1) * (sin th2)) & cos (th1 - th2) = ((cos th1) * (cos th2)) + ((sin th1) * (sin th2)) )
thus sin (th1 - th2) = sin . (th1 + (- th2)) by SIN_COS:def 17
.= ((sin . th1) * (cos . (- th2))) + ((cos . th1) * (sin . (- th2))) by SIN_COS:74
.= ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . (- th2))) by SIN_COS:30
.= ((sin . th1) * (cos . th2)) + ((cos . th1) * (- (sin . th2))) by SIN_COS:30
.= ((sin th1) * (cos . th2)) - ((cos . th1) * (sin . th2)) by SIN_COS:def 17
.= ((sin th1) * (cos th2)) - ((cos . th1) * (sin . th2)) by SIN_COS:def 19
.= ((sin th1) * (cos th2)) - ((cos th1) * (sin . th2)) by SIN_COS:def 19
.= ((sin th1) * (cos th2)) - ((cos th1) * (sin th2)) by SIN_COS:def 17 ; :: thesis: cos (th1 - th2) = ((cos th1) * (cos th2)) + ((sin th1) * (sin th2))
thus cos (th1 - th2) = cos . (th1 + (- th2)) by SIN_COS:def 19
.= ((cos . th1) * (cos . (- th2))) - ((sin . th1) * (sin . (- th2))) by SIN_COS:74
.= ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . (- th2))) by SIN_COS:30
.= ((cos . th1) * (cos . th2)) - ((sin . th1) * (- (sin . th2))) by SIN_COS:30
.= ((cos th1) * (cos . th2)) + ((sin . th1) * (sin . th2)) by SIN_COS:def 19
.= ((cos th1) * (cos th2)) + ((sin . th1) * (sin . th2)) by SIN_COS:def 19
.= ((cos th1) * (cos th2)) + ((sin th1) * (sin . th2)) by SIN_COS:def 17
.= ((cos th1) * (cos th2)) + ((sin th1) * (sin th2)) by SIN_COS:def 17 ; :: thesis: verum