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 )) )
Sum ((th * <i> ) ExpSeq ) = (Sum (Re ((th * <i> ) ExpSeq ))) + ((Sum (Im ((th * <i> ) ExpSeq ))) * <i> ) by COMSEQ_3:54;
then ( Sum (Re ((th * <i> ) ExpSeq )) = Re (Sum ((th * <i> ) ExpSeq )) & Sum (Im ((th * <i> ) ExpSeq )) = Im (Sum ((th * <i> ) ExpSeq )) ) by COMPLEX1:28;
then A1: ( Partial_Sums (Re ((th * <i> ) ExpSeq )) is convergent & lim (Partial_Sums (Re ((th * <i> ) ExpSeq ))) = Re (Sum ((th * <i> ) ExpSeq )) & Partial_Sums (Im ((th * <i> ) ExpSeq )) is convergent & lim (Partial_Sums (Im ((th * <i> ) ExpSeq ))) = Im (Sum ((th * <i> ) ExpSeq )) ) by SERIES_1:def 2, SERIES_1:def 3;

A2: 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
A3: 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 A1, 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 A4: n <= k ; :: thesis: abs (((Partial_Sums (th P_cos )) . k) - (Re (Sum ((th * <i> ) ExpSeq )))) < p
A5: 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 )))) by Th38;
2 * k = k + k ;
hence abs (((Partial_Sums (th P_cos )) . k) - (Re (Sum ((th * <i> ) ExpSeq )))) < p by A3, A4, A5, 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 A6: lim (Partial_Sums (th P_cos )) = Re (Sum ((th * <i> ) ExpSeq )) by A2, SEQ_2:def 7;

A7: 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
A8: 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 A1, 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 A9: n <= k ; :: thesis: abs (((Partial_Sums (th P_sin )) . k) - (Im (Sum ((th * <i> ) ExpSeq )))) < p
A10: 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 A9, 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 A8, A10; :: 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 A7, 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 A2, A6, A7, SEQ_2:def 6, SERIES_1:def 3; :: thesis: verum