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