let th be Real; :: thesis: ( Partial_Sums (th P_sin) is convergent & Sum (th P_sin) = Im (Sum ((th * <i>) ExpSeq)) & Partial_Sums (th P_cos) is convergent & Sum (th P_cos) = Re (Sum ((th * <i>) ExpSeq)) )
A1: Sum ((th * <i>) ExpSeq) = (Sum (Re ((th * <i>) ExpSeq))) + ((Sum (Im ((th * <i>) ExpSeq))) * <i>) by COMSEQ_3:53;
then A2: Sum (Re ((th * <i>) ExpSeq)) = Re (Sum ((th * <i>) ExpSeq)) by COMPLEX1:12;
A3: Sum (Im ((th * <i>) ExpSeq)) = Im (Sum ((th * <i>) ExpSeq)) by A1, COMPLEX1:12;
A4: ( Partial_Sums (Re ((th * <i>) ExpSeq)) is convergent & lim (Partial_Sums (Re ((th * <i>) ExpSeq))) = Re (Sum ((th * <i>) ExpSeq)) ) by A2, SERIES_1:def 2, SERIES_1:def 3;
A5: ( Partial_Sums (Im ((th * <i>) ExpSeq)) is convergent & lim (Partial_Sums (Im ((th * <i>) ExpSeq))) = Im (Sum ((th * <i>) ExpSeq)) ) by A3, SERIES_1:def 2, SERIES_1:def 3;

A6: now :: thesis: for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p

let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for k being Nat st n <= k holds
|.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p )
assume p > 0 ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
|.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p
then consider n being Nat such that
A7: for k being Nat st n <= k holds
|.(((Partial_Sums (Re ((th * <i>) ExpSeq))) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p by A4, SEQ_2:def 7;
take n = n; :: thesis: for k being Nat st n <= k holds
|.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p

now :: thesis: for k being Nat st n <= k holds
|.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p

let k be Nat; :: thesis: ( n <= k implies |.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p )
assume A8: n <= k ; :: thesis: |.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p
( |.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| = |.(((Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * k)) - (Re (Sum ((th * <i>) ExpSeq)))).| & 2 * k = k + k ) by Th34;
hence |.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p by A7, A8, NAT_1:12; :: thesis: verum

end;

hence for k being Nat st n <= k holds
|.(((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))).| < p ; :: thesis: verum

end;

then Partial_Sums (th P_cos) is convergent by SEQ_2:def 6;
then A9: lim (Partial_Sums (th P_cos)) = Re (Sum ((th * <i>) ExpSeq)) by A6, SEQ_2:def 7;

A10: now :: thesis: for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p

let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for k being Nat st n <= k holds
|.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p )
assume p > 0 ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
|.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p
then consider n being Nat such that
A11: for k being Nat st n <= k holds
|.(((Partial_Sums (Im ((th * <i>) ExpSeq))) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p by A5, SEQ_2:def 7;
take n = n; :: thesis: for k being Nat st n <= k holds
|.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p

now :: thesis: for k being Nat st n <= k holds
|.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p

let k be Nat; :: thesis: ( n <= k implies |.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p )
assume A12: n <= k ; :: thesis: |.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p
A13: |.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| = |.(((Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * k) + 1)) - (Im (Sum ((th * <i>) ExpSeq)))).| by Th34;
2 * k = k + k ;
then n <= 2 * k by A12, NAT_1:12;
then n < (2 * k) + 1 by NAT_1:13;
hence |.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p by A11, A13; :: thesis: verum

end;

hence for k being Nat st n <= k holds
|.(((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))).| < p ; :: thesis: verum

end;

then Partial_Sums (th P_sin) is convergent by SEQ_2:def 6;
then lim (Partial_Sums (th P_sin)) = Im (Sum ((th * <i>) ExpSeq)) by A10, SEQ_2:def 7;
hence ( Partial_Sums (th P_sin) is convergent & Sum (th P_sin) = Im (Sum ((th * <i>) ExpSeq)) & Partial_Sums (th P_cos) is convergent & Sum (th P_cos) = Re (Sum ((th * <i>) ExpSeq)) ) by A6, A9, A10, SEQ_2:def 6, SERIES_1:def 3; :: thesis: verum