let V be Z_Module; :: thesis: for v being VECTOR of V
for a being Integer
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
for W being Submodule of V st v in W holds
a * v in W
let a be Integer; :: 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 ;
VW is linearly-closed by Lm3;
then a * v in the carrier of W by A1;
hence a * v in W ; :: thesis: verum