theorem :: VECTSP_2:1

for F being Field holds F is domRing