theorem ThStrict1: :: ZMODUL07:37

for R being Ring
for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
VectQuot (V,W) = VectQuot (V,Ws)