let V be Z_Module; :: thesis: for v being VECTOR of V
for a being integer number
for W being Submodule of V st v in W holds
a * v in W
let v be VECTOR of V; :: thesis: for a being integer number
for W being Submodule of V st v in W holds
a * v in W
let a be integer number ; :: thesis: for W being Submodule of V st v in W holds
a * v in W
let W be Submodule of V; :: thesis: ( v in W implies a * v in W )
reconsider VW = the carrier of W as Subset of V by Def9;
assume v in W ; :: thesis: a * v in W
then A1: v in the carrier of W by STRUCT_0:def 5;
VW is linearly-closed by Lm3;
then a * v in the carrier of W by A1, Def8;
hence a * v in W by STRUCT_0:def 5; :: thesis: verum