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