External evaluation detects tensor-square operations

Let A^d be the degree-d part of the square algebra. By the admissible-basis theorem, its basis consists of Sq^I with |I|=d. Set X_d=(RP^L)^{d+1}, P_d=x₁⋯x_{d+1}, with L≥d+1. Every admissible I of degree d has e(I)≤d<d+1. The leading-monomial lemma therefore applies and gives distinct largest monomials for the classes Sq^I(P_d). Those classes are linearly independent: in a nonzero finite linear combination, the largest of the distinct leading monomials cannot cancel. Thus evaluation j_d:A^d→H*(X_d;F₂), a↦a(P_d), is injective. For d=0, X_0=RP^L and P_0=x₁; the identity operation sends x₁ to the nonzero class x₁.

The map $j_d\otimes j_e$ is injective for an explicit linear-algebra reason. Extend bases of im(j_d) and im(j_e) to bases of the two target vector spaces. Projection to im(j_d), followed by j_d⁻¹, gives a left inverse r_d of j_d; similarly obtain r_e. Then r_d⊗r_e is a left inverse of j_d⊗j_e by the tensor universal property, so j_d⊗j_e is injective. The cohomological Künneth theorem identifies the target with the corresponding external-product subspace in H*(X_d×X_e;F₂). Distinct bidegrees remain distinct under this Künneth decomposition. Since every tensor is a finite sum of homogeneous bidegrees, an element of A⊗A acting as zero on every external product of classes must be zero. This proves tensor faithfulness.