@MISC{ABIAN.MIZ,
  AUTHOR = {Rudnicki, Piotr and Trybulec, Andrzej},
  TITLE = {{A}bian's Fixed Point Theorem},
  NOTE = {This work was partially supported by NSERC Grant OGP9207
		  and NATO CRG 951368.},
  DAY = {22},
  MONTH = {February},
  YEAR = {1997},
  ADDRESS1 = {University of Alberta\\Edmonton},
  ADDRESS2 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {A. Abian \cite{abi68} proved the following theorem:
 \begin{quotation}
Let $f$ be a mapping from a finite set $D$. Then $f$ has a fixed point
if and only if $D$ is not a union of three mutually disjoint sets $A$,
 $B$ and $C$ such that
 \[ A \cap f[A] = B \cap f[B] = C \cap f[C] = \emptyset.\]
 \end{quotation}
(The range of $f$ is not necessarily the subset of its domain).
The proof of the sufficiency is by induction on the number of elements of $D$.
A.~M\c{a}kowski and K.~Wi{\'s}niewski \cite{maw69} have
shown that the assumption of finiteness is superfluous.
They proved their version of the theorem for $f$ being a function
from $D$ into $D$.
In the proof, the required partition was constructed and the
construction used the axiom of choice.
Their main point was to demonstrate that the use of this axiom in the
proof is essential.
We have proved in Mizar the generalized version of Abian's
theorem, i.e. without assuming finiteness of $D$. We have simplified the
proof from \cite{maw69} which uses well-ordering principle and transfinite
ordinals---our proof does not use these notions but otherwise is based
on their idea (we employ choice functions).}}

