for Z being open Subset of REAL
for n being Nat holds
( (diff (sin,Z)) . (2 * n) = ((- 1) |^ n) (#) (sin | Z) & (diff (sin,Z)) . ((2 * n) + 1) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . (2 * n) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . ((2 * n) + 1) = ((- 1) |^ (n + 1)) (#) (sin | Z) )