let n be Nat; :: thesis:
let th be Real; :: thesis:

now :: thesis:

A1: (Partial_Sums (th P_sin)) . 0 = (th P_sin) . 0 by SERIES_1:def 1
.= (((- 1) |^ 0) * (th |^ ((2 * 0) + 1))) / (((2 * 0) + 1) !) by Def20 ;
A2: ((2 * 0) + 1) ! = (0 !) * 1 by NEWTON:15
.= 1 by NEWTON:12 ;
A3: (- 1) |^ 0 = ((- 1) GeoSeq) . 0 by PREPOWER:def 1
.= 1 by PREPOWER:3 ;
A4: (Partial_Sums (th P_cos)) . 0 = (th P_cos) . 0 by SERIES_1:def 1
.= (((- 1) |^ 0) * (th |^ (2 * 0))) / ((2 * 0) !) by Def21
.= (1 * ((th GeoSeq) . 0)) / 1 by A3, NEWTON:12, PREPOWER:def 1
.= 1 by PREPOWER:3 ;
A5: ( (Im ((th * ) ExpSeq)) . 0 = Im (((th * ) ExpSeq) . 0) & (Im ((th * ) ExpSeq)) . 1 = Im (((th * ) ExpSeq) . 1) ) by COMSEQ_3:def 6;
A6: th * = 0 + (th * ) ;
A7: (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * 0) + 1) = ((Partial_Sums (Im ((th * ) ExpSeq))) . 0) + ((Im ((th * ) ExpSeq)) . 1) by SERIES_1:def 1
.= ((Im ((th * ) ExpSeq)) . 0) + ((Im ((th * ) ExpSeq)) . 1) by SERIES_1:def 1
.= 0 + (Im (((th * ) ExpSeq) . (0 + 1))) by A5, Th3, COMPLEX1:6
.= 0 + (Im (((((th * ) ExpSeq) . 0) * (th * )) / ((0 + 1) + (0 * )))) by Th3
.= Im ((1 * (th * )) / 1) by Th3
.= th by A6, COMPLEX1:12 ;
defpred S₁[ Nat] means ( (Partial_Sums (th P_sin)) . $1 = (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * $1) + 1) & (Partial_Sums (th P_cos)) . $1 = (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * $1) );
(Partial_Sums (Re ((th * ) ExpSeq))) . (2 * 0) = (Re ((th * ) ExpSeq)) . 0 by SERIES_1:def 1
.= Re (((th * ) ExpSeq) . 0) by COMSEQ_3:def 5
.= 1 by Th3, COMPLEX1:6 ;
then A8: S₁[ 0 ] by A1, A2, A3, A4, A7;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume that
A10: (Partial_Sums (th P_sin)) . k = (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * k) + 1) and
A11: (Partial_Sums (th P_cos)) . k = (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * k) ; :: thesis:
(Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (Im ((th * ) ExpSeq))) . (((2 * k) + 1) + 1)) + ((Im ((th * ) ExpSeq)) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_sin)) . k) + ((Im ((th * ) ExpSeq)) . (2 * (k + 1)))) + ((Im ((th * ) ExpSeq)) . ((2 * (k + 1)) + 1)) by A10, SERIES_1:def 1
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * ) ExpSeq) . (2 * (k + 1))))) + ((Im ((th * ) ExpSeq)) . ((2 * (k + 1)) + 1)) by COMSEQ_3:def 6
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * ) ExpSeq) . (2 * (k + 1))))) + (Im (((th * ) ExpSeq) . ((2 * (k + 1)) + 1))) by COMSEQ_3:def 6
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * ) |^ (2 * (k + 1))) / ((2 * (k + 1)) !)))) + (Im (((th * ) ExpSeq) . ((2 * (k + 1)) + 1))) by Def4
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * ) |^ (2 * (k + 1))) / ((2 * (k + 1)) !)))) + (Im (((th * ) |^ ((2 * (k + 1)) + 1)) / (((2 * (k + 1)) + 1) !))) by Def4
.= (((Partial_Sums (th P_sin)) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)))) + (Im (((th * ) |^ ((2 * (k + 1)) + 1)) / (((2 * (k + 1)) + 1) !))) by Th33
.= (((Partial_Sums (th P_sin)) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * ) / (((2 * (k + 1)) + 1) !))) by Th33 ;
then (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * (k + 1)) + 1) = (((Partial_Sums (th P_sin)) . k) + (Im (((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) + ((0 / ((2 * (k + 1)) !)) * )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * ) / (((2 * (k + 1)) + 1) !))) ;
then (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * (k + 1)) + 1) = (((Partial_Sums (th P_sin)) . k) + 0) + (Im ((0 / (((2 * (k + 1)) + 1) !)) + (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) !)) * ))) by COMPLEX1:12
.= (((Partial_Sums (th P_sin)) . k) + (0 / ((2 * (k + 1)) !))) + ((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) !)) by COMPLEX1:12 ;
then A12: (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (th P_sin)) . k) + ((th P_sin) . (k + 1)) by Def20
.= (Partial_Sums (th P_sin)) . (k + 1) by SERIES_1:def 1 ;
(Partial_Sums (Re ((th * ) ExpSeq))) . (2 * (k + 1)) = ((Partial_Sums (Re ((th * ) ExpSeq))) . ((2 * k) + 1)) + ((Re ((th * ) ExpSeq)) . (((2 * k) + 1) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . k) + ((Re ((th * ) ExpSeq)) . ((2 * k) + 1))) + ((Re ((th * ) ExpSeq)) . (((2 * k) + 1) + 1)) by A11, SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * ) ExpSeq) . ((2 * k) + 1)))) + ((Re ((th * ) ExpSeq)) . (((2 * k) + 1) + 1)) by COMSEQ_3:def 5
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * ) ExpSeq) . ((2 * k) + 1)))) + (Re (((th * ) ExpSeq) . (((2 * k) + 1) + 1))) by COMSEQ_3:def 5
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * ) |^ ((2 * k) + 1)) / (((2 * k) + 1) !)))) + (Re (((th * ) ExpSeq) . (((2 * k) + 1) + 1))) by Def4
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * ) |^ ((2 * k) + 1)) / (((2 * k) + 1) !)))) + (Re (((th * ) |^ (2 * (k + 1))) / ((((2 * k) + 1) + 1) !))) by Def4
.= (((Partial_Sums (th P_cos)) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * ) / (((2 * k) + 1) !)))) + (Re (((th * ) |^ (2 * (k + 1))) / ((2 * (k + 1)) !))) by Th33
.= (((Partial_Sums (th P_cos)) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * ) / (((2 * k) + 1) !)))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))) by Th33 ;
then (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos)) . k) + (Re ((0 / (((2 * k) + 1) !)) + (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) / (((2 * k) + 1) !)) * )))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))) ;
then (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos)) . k) + (0 / (((2 * k) + 1) !))) + (Re (((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) + ((0 / ((2 * (k + 1)) !)) * ))) by COMPLEX1:12
.= (((Partial_Sums (th P_cos)) . k) + (0 / (((2 * k) + 1) !))) + ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) by COMPLEX1:12 ;
then (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * (k + 1)) = ((Partial_Sums (th P_cos)) . k) + ((th P_cos) . (k + 1)) by Def21
.= (Partial_Sums (th P_cos)) . (k + 1) by SERIES_1:def 1 ;
hence S₁[k + 1] by A12; :: thesis:

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A9); :: thesis:

end;

hence ( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * n) ) ; :: thesis: