theorem ZL2LmSc1: :: ZMODLAT2:58

for L being positive-definite Z_Lattice
for I being Basis of L
for v, w being Vector of L st ( for u being Vector of L st u in I holds
<;u,v;> = <;u,w;> ) holds
for u being Vector of L holds <;u,v;> = <;u,w;>