let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L
for v1, v2 being Vector of L
for w1, w2 being Vector of L1 st w1 = v1 & w2 = v2 holds
w1 - w2 = v1 - v2
let L1 be Z_Sublattice of L; :: thesis: for v1, v2 being Vector of L
for w1, w2 being Vector of L1 st w1 = v1 & w2 = v2 holds
w1 - w2 = v1 - v2
let v1, v2 be Vector of L; :: thesis: for w1, w2 being Vector of L1 st w1 = v1 & w2 = v2 holds
w1 - w2 = v1 - v2
let w1, w2 be Vector of L1; :: thesis: ( w1 = v1 & w2 = v2 implies w1 - w2 = v1 - v2 )
assume AS: ( w1 = v1 & w2 = v2 ) ; :: thesis: w1 - w2 = v1 - v2
L1 is Submodule of L by ThSL1;
hence w1 - w2 = v1 - v2 by AS, ZMODUL01:31; :: thesis: verum