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 being Real st x in ].(- r),r.[ holds
( |.((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)).| < e & |.((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)).| < e )