let R be Ring; 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; 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; ( ( 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
; 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; verum