Unique factorization in chain extensions of semigroups

Cashwell and Everett have shown that, in the ring C [[x1, x2, ...]] of formal power series in a countable number of indeterminates over the field of complex numbers, factorization into irreducibles is unique up to order and units. Their proof makes extensive use of the fact that each P = P(x1, x2...) C[[x1, x2...]] determines a sequence {Pn} of power series in the indeterminates x1, x2 ... xn by Pn(x1,...,xn) = P(x1,..., xn, 0, ...). In particular, Pn(x1,...,xn) = Pn+1(x1,..., xn, 0, ...) and, conversely, each such sequence uniquely determines an element P of C[[x1, x2,...]]. The proof is inductive, using the unique factorisation in C[[x1,... xn]] and the observation that P(x1,..., xn, 0) is a unit if and only if P(x1,..., xn+1, 0) is a unit. In this paper we prove a more general theorem about rings of power series (Th. 6.3). Our method is more direct because we begin by studying semigroups and obtain the power series theorem by specializing one of our main results (Th. 4.6 and Gar. 4.7)