for th being Real holds
( sin is_differentiable_on REAL & diff (sin,th) = cos . th )