theorem :: HFDIFF_1:34

for x, x0 being Real
for n being Element of NAT
for Z being open Subset of REAL st x0 in Z holds
( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )