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

let p be real number ; :: thesis: ( p > 0 implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))) < p )
assume p > 0 ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))) < p
then consider n being Element of NAT such that
A7: for k being Element of NAT st n <= k holds
abs (((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 Element of NAT st n <= k holds
abs (((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))) < p

now

let k be Element of NAT ; :: thesis: ( n <= k implies abs (((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))) < p )
assume A8: n <= k ; :: thesis: abs (((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))) < p
( abs (((Partial_Sums (th P_cos)) . k) - (Re (Sum ((th * <i>) ExpSeq)))) = abs (((Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * k)) - (Re (Sum ((th * <i>) ExpSeq)))) & 2 * k = k + k ) by Th38;
hence abs (((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 Element of NAT st n <= k holds
abs (((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

let p be real number ; :: thesis: ( p > 0 implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))) < p )
assume p > 0 ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))) < p
then consider n being Element of NAT such that
A11: for k being Element of NAT st n <= k holds
abs (((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 Element of NAT st n <= k holds
abs (((Partial_Sums (th P_sin)) . k) - (Im (Sum ((th * <i>) ExpSeq)))) < p

now

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

end;

hence for k being Element of NAT st n <= k holds
abs (((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