theorem Th3: :: COMPLEX2:3

for a, b being Real holds
( sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b)) & cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b)) )