let K be Ring; :: thesis: for V being LeftMod of K holds V is Subspace of (Omega). V
let V be LeftMod of K; :: thesis: V is Subspace of (Omega). V
set W = (Omega). V;
A1: (Omega). V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def 4;
then A2: 0. V = 0. ((Omega). V) ;
dom the lmult of ((Omega). V) = [: the carrier of K, the carrier of ((Omega). V):] by FUNCT_2:def 1;
then A3: the lmult of V = the lmult of ((Omega). V) | [: the carrier of K, the carrier of V:] by A1, RELAT_1:68;
dom the addF of ((Omega). V) = [: the carrier of ((Omega). V), the carrier of ((Omega). V):] by FUNCT_2:def 1;
then the addF of V = the addF of ((Omega). V) || the carrier of V by A1, RELAT_1:68;
hence V is Subspace of (Omega). V by A1, A2, A3, VECTSP_4:def 2; :: thesis: verum