let r, x be Real; :: thesis: for m being Element of NAT st 0 < r holds
( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_sin )) . m & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_cos )) . m )
let m be Element of NAT ; :: thesis: ( 0 < r implies ( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_sin )) . m & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_cos )) . m ) )
assume A1: r > 0 ; :: thesis: ( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_sin )) . m & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_cos )) . m )
thus (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_sin )) . m :: thesis: (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_cos )) . m

proof

defpred S₁[ Element of NAT ] means (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * $1) + 1) = (Partial_Sums (x P_sin )) . $1;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[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 A1, Th20
.= ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (((2 * k) + 1) + 1)) + ((x P_sin ) . (k + 1)) by SIN_COS:def 24
.= (((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * k) + 1)) + ((Maclaurin sin ,].(- r),r.[,x) . (2 * (k + 1)))) + ((x P_sin ) . (k + 1)) by SERIES_1:def 1
.= (((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * k) + 1)) + 0 ) + ((x P_sin ) . (k + 1)) by A1, Th20
.= (Partial_Sums (x P_sin )) . (k + 1) by A3, SERIES_1:def 1 ;
hence S₁[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 A1, Th20
.= (((- 1) |^ 0 ) * (x |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! ) by A1, Th20
.= (x P_sin ) . 0 by SIN_COS:def 24
.= (Partial_Sums (x P_sin )) . 0 by SERIES_1:def 1 ;
then A4: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2);
hence (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_sin )) . m ; :: thesis: verum

end;

defpred S₁[ Element of NAT ] means (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * $1) + 1) = (Partial_Sums (x P_cos )) . $1;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[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 A1, Th20
.= (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
.= ((Partial_Sums (x P_cos )) . k) + ((((- 1) |^ (k + 1)) * (x |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )) by A1, A6, Th20
.= ((Partial_Sums (x P_cos )) . k) + ((x P_cos ) . (k + 1)) by SIN_COS:def 25
.= (Partial_Sums (x P_cos )) . (k + 1) by SERIES_1:def 1 ;
hence S₁[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 A1, Th20
.= (((- 1) |^ 0 ) * (x |^ (2 * 0 ))) / ((2 * 0 ) ! ) by A1, Th20
.= (x P_cos ) . 0 by SIN_COS:def 25
.= (Partial_Sums (x P_cos )) . 0 by SERIES_1:def 1 ;
then A7: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A5);
hence (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) + 1) = (Partial_Sums (x P_cos )) . m ; :: thesis: verum