let a, b be Real; :: thesis: sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b))
thus sin (a - b) = ((sin . a) * (cos . (- b))) + ((cos . a) * (sin . (- b))) by Th73
.= ((sin . a) * (cos . b)) + ((cos . a) * (sin . (- b))) by Th30
.= ((sin . a) * (cos . b)) + ((cos . a) * (- (sin . b))) by Th30
.= ((sin a) * (cos b)) - ((cos a) * (sin b)) ; :: thesis: verum