dom (- sin) = [#] REAL by FUNCT_2:def 1;
hence - sin is_differentiable_on REAL by Th23, SIN_COS:68; :: thesis: verum