theorem :: FDIFF_8:26

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) )