Si consideri l'applicazione lineare $f : V \to\dual W$ tale che $f(\vec v)$ è un funzionale di $\dual W$ tale che
$f(\vec v)(\vec w)=\varphi(\vec v, \vec w)$$\forall\vec w \in W$. Si osserva che $W^\perp=\Ker f$, da cui,
per la formula delle dimensioni, $\dim V =\dim W^\perp+\rg f$. Inoltre, si osserva anche che
$f = i^\top\circ a_\varphi$, dove $i : W \to V$ è tale che $i(\vec w)=\vec w$, infatti $f(\vec v)= a_\varphi(\vec v)\circ i$ è un funzionale di $\dual W$ tale che $f(\vec v)(\vec w)=\varphi(\vec v, \vec w)$. Pertanto
Poiché $\rg(A)=\rg(A^\top)$, si deduce che $\rg(f)=\rg(g)\implies\rg(i^\top\circ a_\varphi)=\rg(a_\varphi\circ i)=\rg(\restr{a_\varphi}{W})=\dim W -\dim\Ker\restr{a_\varphi}{W}=\dim W -\dim(W \cap\underbrace{\Ker a_\varphi}_{V^\perp})=\dim W -\dim(W \cap V^\perp)$. Si conclude allora, sostituendo quest'ultima
identità nell'identità ricavata a inizio dimostrazione che $\dim V =\dim W^\top+\dim W -\dim(W \cap V^\perp)$,
Sia dimostra il teorema per induzione su $n :=\dim V$. Per $n \leq1$, la dimostrazione è triviale. Sia
allora il teorema vero per $i \leq n$. Se $V$ ammette un vettore non isotropo $\vec w$, sia $W =\Span(\vec w)$ e si consideri la decomposizione $V = W \oplus W^\perp$. Poiché $W^\perp$ ha dimensione $n-1$, per ipotesi induttiva
ammette una base ortogonale. Inoltre, tale base è anche ortogonale a $W$, e quindi l'aggiunta di $\vec w$ a
questa base ne fa una base ortogonale di $V$. Se invece $V$ non ammette vettori non isotropi, ogni forma quadratica
è nulla, e quindi il prodotto scalare è nullo per la proposizione precedente.