let K be Ring; :: thesis: for V being LeftMod of K holds VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
let V be LeftMod of K; :: thesis: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
(Omega). V = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def 4;
hence VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V ; :: thesis: verum