A D353: Set automorphism $f : X \to X$ is a permutation on $X$ if and only if there exists a D11: Set $E$ such that

(1)	$E \subseteq X$ is a D78: Subset of $X$
(2)	$E$ is a D17: Finite set
(3)	$\forall \, x \in X \setminus E : f(x) = x$