let th be Real; :: thesis: Sum ((th * <i>) ExpSeq) = (cos . th) + ((sin . th) * <i>)
( Im (Sum ((th * <i>) ExpSeq)) = sin . th & Re (Sum ((th * <i>) ExpSeq)) = cos . th ) by Def16, Def18;
hence Sum ((th * <i>) ExpSeq) = (cos . th) + ((sin . th) * <i>) by COMPLEX1:13; :: thesis: verum