theorem :: HFDIFF_1:55

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