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 the strict Field is domRing-like ;
hence ex b₁ being Ring st
( b₁ is strict & not b₁ is degenerated & b₁ is commutative & b₁ is almost_left_invertible & b₁ is domRing-like ) ; :: thesis: verum