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:54;
A2: Sum (Re ((th * <i> ) ExpSeq )) = Re (Sum ((th * <i> ) ExpSeq )) by A1, COMPLEX1:28;
A3: Sum (Im ((th * <i> ) ExpSeq )) = Im (Sum ((th * <i> ) ExpSeq )) by A1, COMPLEX1:28;
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 A7: 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
consider n being Element of NAT such that
A8: 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, A7, 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

A9: 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 A10: n <= k ; :: thesis: abs (((Partial_Sums (th P_cos )) . k) - (Re (Sum ((th * <i> ) ExpSeq )))) < p
A11: ( 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;
thus abs (((Partial_Sums (th P_cos )) . k) - (Re (Sum ((th * <i> ) ExpSeq )))) < p by A8, A10, A11, NAT_1:12; :: thesis: verum

end;

thus for k being Element of NAT st n <= k holds
abs (((Partial_Sums (th P_cos )) . k) - (Re (Sum ((th * <i> ) ExpSeq )))) < p by A9; :: thesis: verum

end;

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

A14: 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 A15: 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
consider n being Element of NAT such that
A16: 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, A15, 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

A17: 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 A18: n <= k ; :: thesis: abs (((Partial_Sums (th P_sin )) . k) - (Im (Sum ((th * <i> ) ExpSeq )))) < p
A19: 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;
A20: 2 * k = k + k ;
A21: n <= 2 * k by A18, A20, NAT_1:12;
A22: n < (2 * k) + 1 by A21, NAT_1:13;
thus abs (((Partial_Sums (th P_sin )) . k) - (Im (Sum ((th * <i> ) ExpSeq )))) < p by A16, A19, A22; :: thesis: verum

end;

thus for k being Element of NAT st n <= k holds
abs (((Partial_Sums (th P_sin )) . k) - (Im (Sum ((th * <i> ) ExpSeq )))) < p by A17; :: thesis: verum

end;

A23: Partial_Sums (th P_sin ) is convergent by A14, SEQ_2:def 6;
A24: lim (Partial_Sums (th P_sin )) = Im (Sum ((th * <i> ) ExpSeq )) by A14, A23, SEQ_2:def 7;
thus ( 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, A13, A14, A24, SEQ_2:def 6, SERIES_1:def 3; :: thesis: verum