Theorem.
There exists exactly one function
which is alternating multilinear w.r.t. columns and such that
.
Proof.
Uniqueness: Let
be such a function, and let
be an
matrix. Call
the
-th column of
, i.e.
, so that 
Also, let
denote the
-th column vector of the identity matrix.
Now one writes each of the
's in terms of the
, i.e.
.
As
is multilinear, one has

From alternation it follows that any term with repeated indices is zero. The sum can therefore be restricted to tuples with non-repeating indices, i.e. permutations:

Because F is alternating, the columns
can be swapped until it becomes the identity. The sign function
is defined to count the number of swaps necessary and account for the resulting sign change. One finally gets:

as
is required to be equal to
.
Therefore no function besides the function defined by the Leibniz Formula can be a multilinear alternating function with
.
Existence: We now show that F, where F is the function defined by the Leibniz formula, has these three properties.
Multilinear:

Alternating:

For any
let
be the tuple equal to
with the
and
indices switched.
![{\displaystyle {\begin{aligned}F(A)&=\sum _{\sigma \in S_{n},\sigma (j_{1})<\sigma (j_{2})}\left[\operatorname {sgn}(\sigma )\left(\prod _{i=1,i\neq j_{1},i\neq j_{2}}^{n}a_{\sigma (i)}^{i}\right)a_{\sigma (j_{1})}^{j_{1}}a_{\sigma (j_{2})}^{j_{2}}+\operatorname {sgn}(\sigma ')\left(\prod _{i=1,i\neq j_{1},i\neq j_{2}}^{n}a_{\sigma '(i)}^{i}\right)a_{\sigma '(j_{1})}^{j_{1}}a_{\sigma '(j_{2})}^{j_{2}}\right]\\&=\sum _{\sigma \in S_{n},\sigma (j_{1})<\sigma (j_{2})}\left[\operatorname {sgn}(\sigma )\left(\prod _{i=1,i\neq j_{1},i\neq j_{2}}^{n}a_{\sigma (i)}^{i}\right)a_{\sigma (j_{1})}^{j_{1}}a_{\sigma (j_{2})}^{j_{2}}-\operatorname {sgn}(\sigma )\left(\prod _{i=1,i\neq j_{1},i\neq j_{2}}^{n}a_{\sigma (i)}^{i}\right)a_{\sigma (j_{2})}^{j_{1}}a_{\sigma (j_{1})}^{j_{2}}\right]\\&=\sum _{\sigma \in S_{n},\sigma (j_{1})<\sigma (j_{2})}\operatorname {sgn}(\sigma )\left(\prod _{i=1,i\neq j_{1},i\neq j_{2}}^{n}a_{\sigma (i)}^{i}\right)\underbrace {\left(a_{\sigma (j_{1})}^{j_{1}}a_{\sigma (j_{2})}^{j_{2}}-a_{\sigma (j_{1})}^{j_{2}}a_{\sigma (j_{2})}^{j_{_{1}}}\right)} _{=0{\text{, if }}A^{j_{1}}=A^{j_{2}}}\\\\\end{aligned}}}](//wikimedia.org/api/rest_v1/media/math/render/svg/3355a381e8cbfa6bcb10150c9ee4fa675a474183)
Thus if
then
.
Finally,
:

Thus the only alternating multilinear functions with
are restricted to the function defined by the Leibniz formula, and it in fact also has these three properties. Hence the determinant can be defined as the only function
with these three properties.