dom (- cos) = [#] REAL by FUNCT_2:def 1;
hence ( - cos is_differentiable_on REAL & ( for x being Real st x in REAL holds
diff ((- cos),x) = sin . x ) ) by Th23, Th25, SIN_COS:67; :: thesis: verum