set F = the strict Field;
for x, y being Scalar of the strict Field holds
( not x * y = 0. the strict Field or x = 0. the strict Field or y = 0. the strict Field ) by VECTSP_1:12;
then A1: the strict Field is domRing-like ;
reconsider F = the strict Field as Ring ;
thus ex b₁ being Ring st
( b₁ is strict & not b₁ is degenerated & b₁ is commutative & b₁ is almost_left_invertible & b₁ is domRing-like ) by A1; :: thesis: verum