for Z being open Subset of REAL st Z c= dom tan holds
( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z )