A1: |.().| = 0 by ABSVALUE:2;
let n be Nat; :: thesis: for r, x being Real st r > 0 holds
( (Maclaurin (sin,].(- r),r.[,x)) . (2 * n) = 0 & (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) & (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) & (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = 0 )

let r, x be Real; :: thesis: ( r > 0 implies ( (Maclaurin (sin,].(- r),r.[,x)) . (2 * n) = 0 & (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) & (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) & (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = 0 ) )
assume r > 0 ; :: thesis: ( (Maclaurin (sin,].(- r),r.[,x)) . (2 * n) = 0 & (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) & (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) & (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = 0 )
then A2: 0 in ].(0 - r),(0 + r).[ by ;
then A3: 0 in dom (cos | ].(- r),r.[) by Th17;
A4: dom (((- 1) |^ n) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A5: (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = ((((diff (sin,].(- r),r.[)) . ((2 * n) + 1)) . 0) * ((x - 0) |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by TAYLOR_1:def 7
.= (((((- 1) |^ n) (#) (cos | ].(- r),r.[)) . 0) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by Th19
.= ((((- 1) |^ n) * ((cos | ].(- r),r.[) . 0)) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by
.= ((((- 1) |^ n) * ()) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by
.= (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by SIN_COS:30 ;
A6: dom (((- 1) |^ n) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A7: 0 in dom (sin | ].(- r),r.[) by ;
A8: (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = ((((diff (cos,].(- r),r.[)) . (2 * n)) . 0) * ((x - 0) |^ (2 * n))) / ((2 * n) !) by TAYLOR_1:def 7
.= (((((- 1) |^ n) (#) (cos | ].(- r),r.[)) . 0) * (x |^ (2 * n))) / ((2 * n) !) by Th19
.= ((((- 1) |^ n) * ((cos | ].(- r),r.[) . 0)) * (x |^ (2 * n))) / ((2 * n) !) by
.= ((((- 1) |^ n) * ()) * (x |^ (2 * n))) / ((2 * n) !) by
.= (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) by SIN_COS:30 ;
A9: dom (((- 1) |^ (n + 1)) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A10: (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = ((((diff (cos,].(- r),r.[)) . ((2 * n) + 1)) . 0) * ((x - 0) |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by TAYLOR_1:def 7
.= (((((- 1) |^ (n + 1)) (#) (sin | ].(- r),r.[)) . 0) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by Th19
.= ((((- 1) |^ (n + 1)) * ((sin | ].(- r),r.[) . 0)) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by
.= ((((- 1) |^ (n + 1)) * ()) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) by
.= 0 by SIN_COS:30 ;
(Maclaurin (sin,].(- r),r.[,x)) . (2 * n) = ((((diff (sin,].(- r),r.[)) . (2 * n)) . 0) * ((x - 0) |^ (2 * n))) / ((2 * n) !) by TAYLOR_1:def 7
.= (((((- 1) |^ n) (#) (sin | ].(- r),r.[)) . 0) * (x |^ (2 * n))) / ((2 * n) !) by Th19
.= ((((- 1) |^ n) * ((sin | ].(- r),r.[) . 0)) * (x |^ (2 * n))) / ((2 * n) !) by
.= ((((- 1) |^ n) * ()) * (x |^ (2 * n))) / ((2 * n) !) by
.= 0 by SIN_COS:30 ;
hence ( (Maclaurin (sin,].(- r),r.[,x)) . (2 * n) = 0 & (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) & (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) & (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = 0 ) by A5, A8, A10; :: thesis: verum