theorem ThSL18: :: ZMODLAT1:38

for L being Z_Lattice
for L1 being Z_Sublattice of L
for w1, w2 being Vector of L1
for v1, v2 being Vector of L st w1 = v1 & w2 = v2 holds
<;w1,w2;> = <;v1,v2;>