for th being Real holds
( 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)) )