theorem Th27: :: TAYLOR_2:27

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