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 = VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) by VECTSP_4:def 4;
A2: dom the addF of ((Omega). V) = [:the carrier of ((Omega). V),the carrier of ((Omega). V):] by FUNCT_2:def 1;
dom the lmult of ((Omega). V) = [:the carrier of K,the carrier of ((Omega). V):] by FUNCT_2:def 1;
then ( the carrier of V c= the carrier of ((Omega). V) & 0. V = 0. ((Omega). V) & the addF of V = the addF of ((Omega). V) || the carrier of V & the lmult of V = the lmult of ((Omega). V) | [:the carrier of K,the carrier of V:] ) by A1, A2, RELAT_1:97;
hence V is Subspace of (Omega). V by VECTSP_4:def 2; :: thesis: verum