let th be real number ; :: thesis: ( cos is_differentiable_on REAL & diff cos ,th = - (sin . th) )
( [#] REAL is open Subset of REAL & REAL c= dom cos & ( for r being Real st r in REAL holds
cos is_differentiable_in r ) ) by Th68, FUNCT_2:def 1;
hence ( cos is_differentiable_on REAL & diff cos ,th = - (sin . th) ) by Th68, FDIFF_1:16; :: thesis: verum