theorem :: FDIFF_9:20

for n being Nat
for Z being open Subset of REAL st Z c= dom ((#Z n) * sec) & 1 <= n holds
( (#Z n) * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) )