let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L
for v being Vector of L
for a being Element of INT.Ring st v in L1 holds
a * v in L1
let L1 be Z_Sublattice of L; :: thesis: for v being Vector of L
for a being Element of INT.Ring st v in L1 holds
a * v in L1
let v be Vector of L; :: thesis: for a being Element of INT.Ring st v in L1 holds
a * v in L1
let a be Element of INT.Ring; :: thesis: ( v in L1 implies a * v in L1 )
assume AS: v in L1 ; :: thesis: a * v in L1
L1 is Submodule of L by ThSL1;
hence a * v in L1 by AS, ZMODUL01:37; :: thesis: verum