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 Def20, Def22;
hence Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> ) by COMPLEX1:29; :: thesis: verum