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