let n be Nat; :: thesis: for th being Real holds
( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )
let th be Real; :: thesis: ( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )

now :: thesis: for n being Nat holds S₁[n]

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 * <i>) ExpSeq)) . 0 = Im (((th * <i>) ExpSeq) . 0) & (Im ((th * <i>) ExpSeq)) . 1 = Im (((th * <i>) ExpSeq) . 1) ) by COMSEQ_3:def 6;
A6: th * <i> = 0 + (th * <i>) ;
A7: (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * 0) + 1) = ((Partial_Sums (Im ((th * <i>) ExpSeq))) . 0) + ((Im ((th * <i>) ExpSeq)) . 1) by SERIES_1:def 1
.= ((Im ((th * <i>) ExpSeq)) . 0) + ((Im ((th * <i>) ExpSeq)) . 1) by SERIES_1:def 1
.= 0 + (Im (((th * <i>) ExpSeq) . (0 + 1))) by A5, Th3, COMPLEX1:6
.= 0 + (Im (((((th * <i>) ExpSeq) . 0) * (th * <i>)) / ((0 + 1) + (0 * <i>)))) by Th3
.= Im ((1 * (th * <i>)) / 1) by Th3
.= th by A6, COMPLEX1:12 ;
defpred S₁[ Nat] means ( (Partial_Sums (th P_sin)) . $1 = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * $1) + 1) & (Partial_Sums (th P_cos)) . $1 = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * $1) );
(Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * 0) = (Re ((th * <i>) ExpSeq)) . 0 by SERIES_1:def 1
.= Re (((th * <i>) 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: ( S₁[k] implies S₁[k + 1] )
assume that
A10: (Partial_Sums (th P_sin)) . k = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * k) + 1) and
A11: (Partial_Sums (th P_cos)) . k = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * k) ; :: thesis: S₁[k + 1]
(Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (Im ((th * <i>) ExpSeq))) . (((2 * k) + 1) + 1)) + ((Im ((th * <i>) ExpSeq)) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_sin)) . k) + ((Im ((th * <i>) ExpSeq)) . (2 * (k + 1)))) + ((Im ((th * <i>) ExpSeq)) . ((2 * (k + 1)) + 1)) by A10, SERIES_1:def 1
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) ExpSeq) . (2 * (k + 1))))) + ((Im ((th * <i>) ExpSeq)) . ((2 * (k + 1)) + 1)) by COMSEQ_3:def 6
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) ExpSeq) . (2 * (k + 1))))) + (Im (((th * <i>) ExpSeq) . ((2 * (k + 1)) + 1))) by COMSEQ_3:def 6
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) |^ (2 * (k + 1))) / ((2 * (k + 1)) !)))) + (Im (((th * <i>) ExpSeq) . ((2 * (k + 1)) + 1))) by Def4
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) |^ (2 * (k + 1))) / ((2 * (k + 1)) !)))) + (Im (((th * <i>) |^ ((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 * <i>) |^ ((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))) * <i>) / (((2 * (k + 1)) + 1) !))) by Th33 ;
then (Partial_Sums (Im ((th * <i>) 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)) !)) * <i>)))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i>) / (((2 * (k + 1)) + 1) !))) ;
then (Partial_Sums (Im ((th * <i>) 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) !)) * <i>))) 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 * <i>) 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 * <i>) ExpSeq))) . (2 * (k + 1)) = ((Partial_Sums (Re ((th * <i>) ExpSeq))) . ((2 * k) + 1)) + ((Re ((th * <i>) ExpSeq)) . (((2 * k) + 1) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . k) + ((Re ((th * <i>) ExpSeq)) . ((2 * k) + 1))) + ((Re ((th * <i>) ExpSeq)) . (((2 * k) + 1) + 1)) by A11, SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) ExpSeq) . ((2 * k) + 1)))) + ((Re ((th * <i>) ExpSeq)) . (((2 * k) + 1) + 1)) by COMSEQ_3:def 5
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) ExpSeq) . ((2 * k) + 1)))) + (Re (((th * <i>) ExpSeq) . (((2 * k) + 1) + 1))) by COMSEQ_3:def 5
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) |^ ((2 * k) + 1)) / (((2 * k) + 1) !)))) + (Re (((th * <i>) ExpSeq) . (((2 * k) + 1) + 1))) by Def4
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) |^ ((2 * k) + 1)) / (((2 * k) + 1) !)))) + (Re (((th * <i>) |^ (2 * (k + 1))) / ((((2 * k) + 1) + 1) !))) by Def4
.= (((Partial_Sums (th P_cos)) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i>) / (((2 * k) + 1) !)))) + (Re (((th * <i>) |^ (2 * (k + 1))) / ((2 * (k + 1)) !))) by Th33
.= (((Partial_Sums (th P_cos)) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i>) / (((2 * k) + 1) !)))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))) by Th33 ;
then (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos)) . k) + (Re ((0 / (((2 * k) + 1) !)) + (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) / (((2 * k) + 1) !)) * <i>)))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))) ;
then (Partial_Sums (Re ((th * <i>) 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)) !)) * <i>))) 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 * <i>) 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: verum

end;

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

end;

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