let r, e be Real; :: thesis:
assume that
A1: r > 0 and
A2: e > 0 ; :: thesis:
consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff sin ,].(- r),r.[) . m) . (s * x)) * (x |^ m)) / (m ! )) < e & abs (((((diff cos ,].(- r),r.[) . m) . (s * x)) * (x |^ m)) / (m ! )) < e ) by A1, A2, Th23;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A4: n <= m ; :: thesis:
A5: ( sin is_differentiable_on m + 1,].(- r),r.[ & cos is_differentiable_on m + 1,].(- r),r.[ ) by Th21;
( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;
then X: ( ].(- r),r.[ c= dom sin & ].(- r),r.[ c= dom cos ) ;

let x be Real; :: thesis:
assume A6: x in ].(- r),r.[ ; :: thesis:
consider s being Real such that
A7: ( 0 < s & s < 1 ) and
A8: abs ((sin . x) - ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . m)) = abs (((((diff sin ,].(- r),r.[) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) ! )) by A1, A5, A6, Th4, X;
m <= m + 1 by NAT_1:11;
then A9: n <= m + 1 by A4, XXREAL_0:2;
hence abs ((sin . x) - ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . m)) < e by A3, A6, A7, A8; :: thesis:
consider s being Real such that
A10: ( 0 < s & s < 1 ) and
A11: abs ((cos . x) - ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . m)) = abs (((((diff cos ,].(- r),r.[) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) ! )) by A1, A5, A6, Th4, X;
thus abs ((cos . x) - ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . m)) < e by A3, A6, A9, A10, A11; :: thesis:

end;

hence for x being real number st x in ].(- r),r.[ holds
( abs ((sin . x) - ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . m)) < e ) ; :: thesis: