theorem :: HFDIFF_1:62

for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z)