theorem Th1: :: INTEGR14:1

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