for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Element of V .. W ex a being Vector of V st x = a .. W