  A special final coalgebra theorem, in the style of Aczel's, is proved within
standard Zermelo-Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced
by a variant definition of function that admits non-well-founded constructions.
Variant ordered pairs and tuples, of possibly infinite length, are special
cases of variant functions. Analogues of Aczel's Solution and Substitution
Lemmas are proved in the style of Rutten and Turi. The approach is less general
than Aczel's, but the treatment of non-well-founded objects is simple and
concrete. The final coalgebra of a functor is its greatest fixedpoint. The
theory is intended for machine implementation and a simple case of it is
already implemented using the theorem prover Isabelle.
