A transgressive simple fiber system gives a polynomial base

For each index form an abstract spectral sequence with initial page $\mathrm{\Lambda }(x_{\lambda })\otimes {\mathbb{F}}_2[Y_{\lambda }],\mathrm{\mid }{x}_{\lambda }\mathrm{\mid }=(0,d_{\lambda }),\mathrm{\mid }{Y}_{\lambda }\mathrm{\mid }=(d_{\lambda }+1,0),$ where $d_{\lambda }=\mathrm{\mid }{x}_{\lambda }\mathrm{\mid }$. All differentials vanish except at $r=d_{\lambda }+1$, where $d_r(x_{\lambda }{Y}_{\lambda }^t)=Y_{\lambda }^{t+1}$ and $d_r(Y_{\lambda }^t)=0$ for every $t\ge 0$.

That differential has bidegree $(r,1-r)$ and square zero. Its homology is the scalar field in $(0,0)$: multiplication by $Y_{\lambda }$ is injective on the polynomial ring, and its cokernel is its constant term. Tensor the factor sequences and use the sum of the factor differentials. In each fixed total degree only finitely many factors can contribute, because their degrees are positive and degreewise locally finite. Homology of these tensor complexes is the tensor of the factor homologies: over a field, cor-every-vector-space-has-a-basis and AC choose bases of boundaries and cycles and extend them to degreewise bases, splitting each complex into its homology and pairs on which the differential is an isomorphism. The tensor universal property makes the maps induced by those linear splittings well defined; thm-tensor-products-commute-with-arbitrary-direct-sums and the tensor-unit theorem distribute the splitting over the tensor factors. Tensoring a contractible pair admits the tensor contracting homotopy $H\otimes \mathrm{i}\mathrm{d}$: the two cross-differential terms cancel in characteristic two, leaving $dH+Hd=\mathrm{i}\mathrm{d}$ on that summand. These constructions use the listed published basis/tensor interfaces, not an unproved tensor-homology formula. This proves the required page-to-page homology condition, including all finite truncations. Thus the tensor is a well-defined first-quadrant spectral sequence with limiting page only ${\mathbb{F}}_2$ in $(0,0)$.

The actual Serre $E_2$ page is $H^{\ast }(B)\otimes H^{\ast }(F)$. Indeed the fiber groups are finite-dimensional in each degree by the simple-system hypothesis; a chosen finite basis identifies the constant coefficient system with a finite direct sum of the scalar system, and cochains and cohomology commute with that finite direct sum. The base is simply connected, so there is no monodromy. No finite-dimensional hypothesis on base cohomology is needed.

Define a linear $E_2$ map by evaluating a squarefree monomial in the formal $x_{\lambda }$ at the corresponding product of actual fiber classes and a polynomial in the $Y_{\lambda }$ at the $y_{\lambda }$. It need not be a ring map on the whole page: formal $x_{\lambda }^2=0$ need not hold in fiber cohomology. The relative-lifts lemma gives the survival of each image $x_{\lambda }$ through its designated page and its differential $y_{\lambda }$ there. The actual differential's Leibniz rule shows, on each squarefree monomial, precisely the sum of factor differentials in the abstract model. Thus the linear map commutes with the first differential and descends to homology. Repeat on each subsequent page: factors already killed have both $x_{\lambda }$ and $Y_{\lambda }$ absent, while every remaining generator survives until its specified page and has the specified differential. The same squarefree-monomial calculation proves commutation and descent at every page. This constructs an actual morphism of spectral sequences, without asserting a false multiplicative map in the fiber direction.

On the fiber axis this map is a vector-space isomorphism by the simple-system hypothesis. On the limiting page it is an isomorphism because the actual sequence strongly converges to cohomology of the contractible total space, while the model has the same scalar limiting page. The fiber-limit comparison now proves the base-axis map at $E_2$ is an isomorphism. On that axis the map really is the polynomial ring homomorphism $Y_{\lambda }\mapsto y_{\lambda }$, so this is the desired algebra isomorphism. The conclusion is a statement on $E_2$, not an unsupported splitting of an abutment filtration.