let R be Ring; :: thesis: for V being LeftMod of R
for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds
W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let V be LeftMod of R; :: thesis: for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds
W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let W be strict Submodule of V; :: thesis: ( ( for v being Vector of V holds v in W ) implies W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
assume for v being Vector of V holds v in W ; :: thesis: W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
then for v being Vector of V holds
( v in W iff v in (Omega). V ) ;
hence W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Th46; :: thesis: verum