theorem :: HFDIFF_1:35

for x, r being Real
for n being Element of NAT st r > 0 holds
( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )