Extremely long answer: The Clifford algebra and the Chevalley map - a computational approach Theorem 1 (or 2, or even 3). Actually the reason for writing this text was my disappointment with the wrong proof in Lawson-Michelson, and with the not sufficiently general proofs in the rest of literature. The heuristics for finding the proof are explained in §6.3 of my diploma thesis to be (unless I mess up the applied maths exam ;) ).
Yes, 90% of the proof are computations.
Now chances are high that you prefer a 1-page proof that works over $\mathbb R$ to a 40-pages one that works over any commutative ring, so you might be interested in the proof that uses orthogonal decomposition of the quadratic form (i. e., finding an orthogonal basis using Gram-Schmidt) and application of the fact that $\mathrm{Cl}\left(V\oplus W\right)\cong \left(\mathrm{Cl}V\right)\hat{\otimes}\left(\mathrm{Cl}W\right)$ (super-tensor product of superalgebras) for any two quadratic spaces $V$ and $W$. Such a proof can be found in Milne's ALA Theorem 18.18, and probably in many other places. As Guntram pointed out in the comment below, this proof only works for $V$ being finite-dimensional; however, the infinite-dimensional case follows from the fact that (unless I am mistaken) taking the Clifford algebra commutes with the direct limit. (Here we are using the fact that if $V$ and $W$ are two finite-dimensional quadratic spaces such that $V\subseteq W$, then the canonical map $\mathrm{Cl}V\to \mathrm{Cl}W$ is injective. This easily follows from the basis theorem for Clifford algebras of finite-dimensional quadratic spaces.)
