theorem Th14: :: HFDIFF_1:14

for x being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2))