theorem :: HFDIFF_1:13

for x being Real
for Z being open Subset of REAL st x in Z holds
((diff (cos,Z)) . 3) . x = sin . x