For endofunctors of many-sorted sets the iterative construction of
terminal coalgebras is proved to converge whenever a terminal
coalgebra exists. The existence of a fixed point is, by Lambek's Lemma,
a necessary condition; we prove that in case of one sort the existence of
two successor fixed points is sufficient for terminal coalgebras.

As demonstrated by James Worell the number of steps needed
for the finite power-set functor is $\omega + \omega$. In
contrast, the initial algebra construction takes, for any
endofunctor of many-sorted sets, a cardinal number of steps.
Joint work with Vera Trnkova.