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