theorem Th22: :: TAYLOR_2:22

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