 Noncommutative formal power series

A noncommutative formal power series is an element of a noncommutative formal power series ring. Its constant term is the coefficient of the empty word. Formal sums are interpreted coefficient by coefficient; analytic convergence is not required.