theorem :: HFDIFF_1:68

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