theorem Th7: :: INTEGR14:7

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) sec) holds
( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) )