theorem Th53: :: INTEGR11:53

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) ) )