:: deftheorem Def3 defines base VECTSP_7:def 3 :
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being LeftMod of GF
for A being Subset of V holds
( A is base iff ( A is linearly-independent & Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) );