( - cos is_differentiable_on REAL & ( for x being Real st x in REAL holds
diff ((- cos),x) = sin . x ) )