theorem :: HFDIFF_1:53

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