theorem :: HFDIFF_1:9

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