let R be Ring; :: thesis: for Y being LeftMod of R
for A being Subset of Y holds Lin A is strict Subspace of (Omega). Y
let Y be LeftMod of R; :: thesis: for A being Subset of Y holds Lin A is strict Subspace of (Omega). Y
let A be Subset of Y; :: thesis: Lin A is strict Subspace of (Omega). Y
U1: ( the carrier of (Lin A) c= the carrier of Y & 0. (Lin A) = 0. Y & the addF of (Lin A) = the addF of Y || the carrier of (Lin A) & the lmult of (Lin A) = the lmult of Y | [: the carrier of R, the carrier of (Lin A):] ) by VECTSP_4:def 2;
( the carrier of Y = the carrier of ((Omega). Y) & 0. Y = 0. ((Omega). Y) & the addF of Y = the addF of ((Omega). Y) & the lmult of Y = the lmult of ((Omega). Y) ) ;
hence Lin A is strict Subspace of (Omega). Y by U1, VECTSP_4:def 2; :: thesis: verum