for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being LeftMod of GF
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I