theorem Th55: :: INTEGR11:55

for Z being open Subset of REAL st Z c= dom (((id Z) - tan) - sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( ((id Z) - tan) - sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) - tan) - sec) `| Z) . x = (sin . x) / ((sin . x) - 1) ) )