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