let F be Field; :: thesis: F is domRing
for x, y being Scalar of F holds
( not x * y = 0. F or x = 0. F or y = 0. F ) by VECTSP_1:12;
hence F is domRing by Def1; :: thesis: verum