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