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

let m be Nat; :: thesis: ( 0 < r implies ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) + 1) = () . m & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = () . m ) )
assume A1: r > 0 ; :: thesis: ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) + 1) = () . m & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = () . m )
thus (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) + 1) = () . m :: thesis: (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = () . m
proof
defpred S1[ Nat] means (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * \$1) + 1) = () . \$1;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
(Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * k) + 2)) + ((Maclaurin (sin,].(- r),r.[,x)) . ((2 * k) + 3)) by SERIES_1:def 1
.= ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * k) + 2)) + ((((- 1) |^ (k + 1)) * (x |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) !)) by
.= ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (((2 * k) + 1) + 1)) + (() . (k + 1)) by SIN_COS:def 20
.= (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * k) + 1)) + ((Maclaurin (sin,].(- r),r.[,x)) . (2 * (k + 1)))) + (() . (k + 1)) by SERIES_1:def 1
.= (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * k) + 1)) + 0) + (() . (k + 1)) by
.= () . (k + 1) by ;
hence S1[k + 1] ; :: thesis: verum
end;
(Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * 0) + 1) = ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * 0)) + ((Maclaurin (sin,].(- r),r.[,x)) . ((2 * 0) + 1)) by SERIES_1:def 1
.= ((Maclaurin (sin,].(- r),r.[,x)) . (2 * 0)) + ((Maclaurin (sin,].(- r),r.[,x)) . ((2 * 0) + 1)) by SERIES_1:def 1
.= 0 + ((Maclaurin (sin,].(- r),r.[,x)) . ((2 * 0) + 1)) by
.= (((- 1) |^ 0) * (x |^ ((2 * 0) + 1))) / (((2 * 0) + 1) !) by
.= () . 0 by SIN_COS:def 20
.= () . 0 by SERIES_1:def 1 ;
then A4: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A2);
hence (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) + 1) = () . m ; :: thesis: verum
end;
defpred S1[ Nat] means (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * \$1) + 1) = () . \$1;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 2)) + ((Maclaurin (cos,].(- r),r.[,x)) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 2)) + 0 by
.= (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (((2 * k) + 1) + 1)
.= ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 1)) + ((Maclaurin (cos,].(- r),r.[,x)) . ((2 * k) + 2)) by SERIES_1:def 1
.= (() . k) + ((((- 1) |^ (k + 1)) * (x |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) by A1, A6, Th20
.= (() . k) + (() . (k + 1)) by SIN_COS:def 21
.= () . (k + 1) by SERIES_1:def 1 ;
hence S1[k + 1] ; :: thesis: verum
end;
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * 0) + 1) = ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * 0)) + ((Maclaurin (cos,].(- r),r.[,x)) . ((2 * 0) + 1)) by SERIES_1:def 1
.= ((Maclaurin (cos,].(- r),r.[,x)) . (2 * 0)) + ((Maclaurin (cos,].(- r),r.[,x)) . ((2 * 0) + 1)) by SERIES_1:def 1
.= ((Maclaurin (cos,].(- r),r.[,x)) . (2 * 0)) + 0 by
.= (((- 1) |^ 0) * (x |^ (2 * 0))) / ((2 * 0) !) by
.= () . 0 by SIN_COS:def 21
.= () . 0 by SERIES_1:def 1 ;
then A7: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A7, A5);
hence (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = () . m ; :: thesis: verum