let r, x be Real; :: thesis: for m being Nat st 0 < r holds
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m
let m be Nat; :: thesis: ( 0 < r implies (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m )
assume A1: r > 0 ; :: thesis: (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m
defpred S₁[ Nat] means (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * $1) = (Partial_Sums (x P_cos)) . $1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
thus (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * (k + 1)) = ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 1)) + ((Maclaurin (cos,].(- r),r.[,x)) . (((2 * k) + 1) + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 1)) + ((((- 1) |^ (k + 1)) * (x |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) by A1, Th20
.= ((Partial_Sums (x P_cos)) . k) + ((((- 1) |^ (k + 1)) * (x |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) by A1, Th25
.= ((Partial_Sums (x P_cos)) . k) + ((x P_cos) . (k + 1)) by SIN_COS:def 21
.= (Partial_Sums (x P_cos)) . (k + 1) by SERIES_1:def 1 ; :: thesis: verum

end;

(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * 0) = (Maclaurin (cos,].(- r),r.[,x)) . (2 * 0) by SERIES_1:def 1
.= (((- 1) |^ 0) * (x |^ (2 * 0))) / ((2 * 0) !) by A1, Th20
.= (x P_cos) . 0 by SIN_COS:def 21
.= (Partial_Sums (x P_cos)) . 0 by SERIES_1:def 1 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m ; :: thesis: verum