theorem :: HFDIFF_1:65

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