let r, e be Real; :: thesis: ( 0 < r & 0 < e implies 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 ) )

assume that
A1: r > 0 and
A2: e > 0 ; :: thesis: 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 )

consider n being Nat such that
A3: 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 ) by A1, A2, Th23;
take n ; :: thesis: 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 )

let m be Nat; :: thesis: ( n <= m implies 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 ) )

assume A4: n <= m ; :: thesis: 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 )

A5: ( cos is_differentiable_on m + 1,].(- r),r.[ & dom cos = REAL ) by ;
A6: ( sin is_differentiable_on m + 1,].(- r),r.[ & dom sin = REAL ) by ;
now :: thesis: 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 )
m <= m + 1 by NAT_1:11;
then A7: n <= m + 1 by ;
let x be Real; :: thesis: ( x in ].(- r),r.[ implies ( |.((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)).| < e & |.((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)).| < e ) )
assume A8: x in ].(- r),r.[ ; :: thesis: ( |.((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)).| < e & |.((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)).| < e )
ex s being Real st
( 0 < s & s < 1 & |.((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)).| = |.(((((diff (sin,].(- r),r.[)) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) !)).| ) by A1, A6, A8, Th4;
hence |.((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)).| < e by A3, A8, A7; :: thesis: |.((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)).| < e
ex s being Real st
( 0 < s & s < 1 & |.((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)).| = |.(((((diff (cos,].(- r),r.[)) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) !)).| ) by A1, A5, A8, Th4;
hence |.((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)).| < e by A3, A8, A7; :: thesis: verum
end;
hence 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 ) ; :: thesis: verum