for R 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 R
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )