Let ${\displaystyle U}$  and ${\displaystyle W}$  be finite subsets of a vector space ${\displaystyle V}$ . If ${\displaystyle U}$  is a set of linearly independent vectors, and ${\displaystyle W}$  spans ${\displaystyle V}$ , then:

1. ${\displaystyle |U|\leq |W|}$ ;

2. There is a set ${\displaystyle W'\subseteq W}$  with ${\displaystyle |W'|=|W|-|U|}$  such that ${\displaystyle U\cup W'}$  spans ${\displaystyle V}$ .

Suppose ${\displaystyle U=\{u_{1},\dots ,u_{m}\}}$  and ${\displaystyle W=\{w_{1},\dots ,w_{n}\}}$ . We wish to show that ${\displaystyle m\leq n}$ , and that after rearranging the ${\displaystyle w_{j}}$  if necessary, the set ${\displaystyle \{u_{1},\dotsc ,u_{m},w_{m+1},\dotsc ,w_{n}\}}$  spans ${\displaystyle V}$ . We proceed by induction on ${\displaystyle m}$ .

For the base case, suppose ${\displaystyle m}$  is zero. In this case, the claim holds because there are no vectors ${\displaystyle u_{i}}$ , and the set ${\displaystyle \{w_{1},\dotsc ,w_{n}\}}$  spans ${\displaystyle V}$  by hypothesis.

For the inductive step, assume the proposition is true for ${\displaystyle m-1}$ . By the inductive hypothesis we may reorder the ${\displaystyle w_{i}}$  so that ${\displaystyle \{u_{1},\ldots ,u_{m-1},w_{m},\ldots ,w_{n}\}}$  spans ${\displaystyle V}$ . Since ${\displaystyle u_{m}\in V}$ , there exist coefficients ${\displaystyle \mu _{1},\ldots ,\mu _{n}}$  such that

${\displaystyle u_{m}=\sum _{i=1}^{m-1}\mu _{i}u_{i}+\sum _{j=m}^{n}\mu _{j}w_{j}}$ .

At least one of the ${\displaystyle \mu _{j}}$  must be non-zero, since otherwise this equality would contradict the linear independence of ${\displaystyle \{u_{1},\ldots ,u_{m}\}}$ ; it follows that ${\displaystyle m\leq n}$ . By reordering ${\displaystyle \mu _{m}w_{m},\ldots ,\mu _{n}w_{n}}$  if necessary, we may assume that ${\displaystyle \mu _{m}}$  is nonzero. Therefore, we have

${\displaystyle w_{m}={\frac {1}{\mu _{m}}}\left(u_{m}-\sum _{j=1}^{m-1}\mu _{j}u_{j}-\sum _{j=m+1}^{n}\mu _{j}w_{j}\right)}$ .

In other words, ${\displaystyle w_{m}}$  is in the span of ${\displaystyle \{u_{1},\ldots ,u_{m},w_{m+1},\ldots ,w_{n}\}}$ . Since this span contains each of the vectors ${\displaystyle u_{1},\ldots ,u_{m-1},w_{m},w_{m+1},\ldots ,w_{n}}$ , by the inductive hypothesis it contains ${\displaystyle V}$ .

The Steinitz exchange lemma is a basic result in computational mathematics, especially in linear algebra and in combinatorial algorithms.^[3]

• Julio R. Bastida, Field extensions and Galois Theory, Addison–Wesley Publishing Company (1984).

• Mizar system proof: http://mizar.org/version/current/html/vectsp_9.html#T19