let th1, th2 be real number ; :: 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 21
.= ((sin . th1) * (cos . (- th2))) + ((cos . th1) * (sin . (- th2))) by SIN_COS:79
.= ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . (- th2))) by SIN_COS:33
.= ((sin . th1) * (cos . th2)) + ((cos . th1) * (- (sin . th2))) by SIN_COS:33
.= ((sin th1) * (cos . th2)) - ((cos . th1) * (sin . th2)) by SIN_COS:def 21
.= ((sin th1) * (cos th2)) - ((cos . th1) * (sin . th2)) by SIN_COS:def 23
.= ((sin th1) * (cos th2)) - ((cos th1) * (sin . th2)) by SIN_COS:def 23
.= ((sin th1) * (cos th2)) - ((cos th1) * (sin th2)) by SIN_COS:def 21 ; :: thesis: cos (th1 - th2) = ((cos th1) * (cos th2)) + ((sin th1) * (sin th2))
thus cos (th1 - th2) = cos . (th1 + (- th2)) by SIN_COS:def 23
.= ((cos . th1) * (cos . (- th2))) - ((sin . th1) * (sin . (- th2))) by SIN_COS:79
.= ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . (- th2))) by SIN_COS:33
.= ((cos . th1) * (cos . th2)) - ((sin . th1) * (- (sin . th2))) by SIN_COS:33
.= ((cos th1) * (cos . th2)) + ((sin . th1) * (sin . th2)) by SIN_COS:def 23
.= ((cos th1) * (cos th2)) + ((sin . th1) * (sin . th2)) by SIN_COS:def 23
.= ((cos th1) * (cos th2)) + ((sin th1) * (sin . th2)) by SIN_COS:def 21
.= ((cos th1) * (cos th2)) + ((sin th1) * (sin th2)) by SIN_COS:def 21 ; :: thesis: verum