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.
Per il teorema di Lagrange, esiste una base ortogonale $\basis'$ di $V$.
Si riordini la base in modo tale che la forma quadratica valutata nei primi elementi sia strettamente positiva, che nei secondi elementi sia strettamente negativa e che negli ultimi sia nulla. Si sostituisca
$\basis'$ con una base $\basis$ tale per cui, se $q(\vv i) > 0$,
allora $\vv i \mapsto\frac{\vv i}{\sqrt{q(\vv i)}}$; se
$q(\vv i) < 0$, allora $\vv i \mapsto\frac{\vv i}{\sqrt{-q(\vv i)}}$;
altrimenti $\vv i \mapsto\vv i$. Si è allora trovata una base
la cui matrice associata del prodotto scalare è come desiderata nella
Sia ora $a$ il numero di vettori della base con forma quadratica
positiva, $b$ il numero di vettori con forma negativa e $c$ quello
dei vettori con forma nulla. Si consideri $W_+=\Span(\vv1, ..., \vv a)$, $W_-=\Span(\vv{a+1}, ..., \vv b)$, $W_0=\Span(\vv{b+1}, ..., \vv c)$. \\
Sia $M = M_\basis(\varphi)$. Si osserva che $c = n -\rg(M)=\dim\Ker(M)=\dim V^\perp=\iota_0$. Inoltre $\forall\v\in W_+$, dacché
$\basis$ è ortogonale,
$q(\v)= q(\sum_{i=1}^a \alpha_i \vv i)=\sum_{i=1}^a \alpha_i^2 q(\vv i) > 0$, e quindi $\restr{\varphi}{W_+} > 0$, da cui $\iota_+\geq a$.
Analogamente $\iota_-\geq b$. \\
Si mostra ora che è impossibile che $\iota_+ > a$. Se così infatti
fosse, sia $W$ tale che $\dim W =\iota_+$ e che $\restr{\varphi}{W} > 0$. $\iota_++ b + c$ sarebbe maggiore di $a + b + c = n :=\dim V$. Quindi, per la formula di Grassman, $\dim(W + W_-+ W_0)=\dim W +
\dim(W_- + W_0) - \dim (W \cap (W_- + W_0)) \implies\dim (W \cap (W_- + W_0)) = \dim W +
tra loro. Analogamente vale il viceversa, dal momento che ogni
base ortogonale di due matrici congruenti devono contenere gli
stessi numeri $\iota_+$, $\iota_-$ e $\iota_0$ di vettori
di base con forma quadratica positiva, negativa e nulla. \\
\li Se $\ww1$, ..., $\ww k$ sono tutti i vettori di una base
ortogonale $\basis$ con forma quadratica nulla, si osserva che $W =\Span(\ww1, ..., \ww k)$ altro non è che $V^\perp$ stesso. Infatti, come
visto anche nella dimostrazione del teorema di Sylvester reale, vale
che $\dim W =\dim\Ker(M_\basis(\varphi))=\dim V^\perp$. Inoltre,
se $\w\in W$ e $\v\in V$, $\varphi(\w, \v)=\varphi(\sum_{i=1}^k \alpha_i \ww i, \sum_{i=1}^k \beta_i \ww i +\sum_{i=k+1}^n \beta_i \vv i)=\sum_{i=1}^k \alpha_i \beta_i q(\ww i)=0$, e quindi
$W \subseteq V^\perp$, da cui si conclude che $W = V^\perp$. \\
\li Vale in particolare che $\rg(\varphi)=\iota_++\iota_-$, mentre
$\dim\Ker(\varphi)=\iota_0$, e quindi $n =\iota_++\iota_-+\iota_0$.
