let r, x be Real; :: thesis: for m being Nat st 0 < r & m > 0 holds
( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = () . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = () . m )

let m be Nat; :: thesis: ( 0 < r & m > 0 implies ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = () . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = () . m ) )
assume that
A1: r > 0 and
A2: m > 0 ; :: thesis: ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = () . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = () . m )
A3: m - 1 is Element of NAT by ;
2 * m > 2 * 0 by ;
then A4: (2 * m) - 1 is Element of NAT by NAT_1:20;
then A5: (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) - 1)) + ((Maclaurin (sin,].(- r),r.[,x)) . (((2 * m) - 1) + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) - 1)) + 0 by
.= (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * (m - 1)) + 1)
.= () . (m - 1) by A1, A3, Th25 ;
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) - 1)) + ((Maclaurin (cos,].(- r),r.[,x)) . (((2 * m) - 1) + 1)) by
.= ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) - 1)) + ((((- 1) |^ m) * (x |^ (2 * m))) / ((2 * m) !)) by
.= ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * (m - 1)) + 1)) + (() . m) by SIN_COS:def 21
.= (() . (m - 1)) + (() . ((m - 1) + 1)) by A1, A3, Th25
.= () . m by ;
hence ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = () . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = () . m ) by A5; :: thesis: verum