for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Vector of (V / W) ex a being Vector of V st x = a / W