theorem Th23: :: TAYLOR_2:23

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e )