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;
then A2: Sum (Re ((th * <i> ) ExpSeq )) = Re (Sum ((th * <i> ) ExpSeq )) by 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 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
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, 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 A10: 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 A8, A10, 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 A13: lim (Partial_Sums (th P_cos )) = Re (Sum ((th * <i> ) ExpSeq )) by A6, 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 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
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, 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 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;
2 * k = k + k ;
then n <= 2 * k by A18, 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 A16, A19; :: 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 A14, 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, A13, A14, SEQ_2:def 6, SERIES_1:def 3; :: thesis: verum