theorem :: HFDIFF_1:54

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