:: deftheorem defines free VECTSP_7:def 4 :
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for IT being LeftMod of GF holds
( IT is free iff ex B being Subset of IT st B is base );