theorem :: HFDIFF_1:58

for Z being open Subset of REAL st Z c= dom tan holds
(diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z)