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