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:72; :: thesis: verum