:: deftheorem Def1 defines dim VECTSP_9:def 1 :
for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for b₃ being Nat holds
( b₃ = dim V iff for I being Basis of V holds b₃ = card I );