theorem :: VECTSP_6:49

for GF being Field holds - (1. GF) <> 0. GF by Lm3;