let K be Ring; :: thesis: for V being LeftMod of K holds ModuleStr(# 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: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
(Omega). V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def 4;
hence ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V ; :: thesis: verum