Soit [formule] un opérateur compact auto-adjoint sur un Hilbert séparable. Montrer que [formule] possède une valeur propre [formule] avec [formule].
Considérer une suite maximisante pour [formule] sur la sphère unité.
Posons [formule] (car [formule]). Soit [formule] une suite avec [formule] et [formule]. Quitte à extraire, [formule] avec [formule] ([formule] car [formule] auto-adjoint). [formule]. Par compacité de [formule] : [formule]. Donc [formule], soit [formule]. [formule] avec [formule] : [formule] est valeur propre. [formule]