theorem :: FDIFF_8:27

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