Cartan proves reflection factorization by an induction that enlarges the fixed subspace. The subgroup-valued statement below is a formalized TauCeti lemma extracted from that method. Cartan's one- or two-reflection correction is repackaged as an element of \(H\) acting trivially on \(W+Kx\).
Let \(K\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on a \(K\)-vector space \(V\), and let \(H\le O(V,Q)\) contain every reflection in a nonisotropic vector. Suppose \(g\in O(V,Q)\) fixes a subspace \(W\) pointwise and \(x\in W^{\perp }\) has \(Q(x)\ne 0\). Then there is an element \(r\in H\) such that
\[rg\vert _{W+Kx}=\operatorname {id}.\]
The correction leaves the previously fixed space untouched and fixes one additional nonisotropic direction. It is either one reflection or a product of two reflections.