let th be Real; :: thesis: Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> )
A1: Im (Sum ((th * <i> ) ExpSeq )) = sin . th by Def20;
Re (Sum ((th * <i> ) ExpSeq )) = cos . th by Def22;
hence Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> ) by A1, COMPLEX1:29; :: thesis: verum