theorem ZL2ThSc1: :: ZMODLAT2:59

for L being positive-definite Z_Lattice
for b being OrdBasis of L
for v, w being Vector of L st ( for n being Nat st n in dom b holds
<;(b /. n),v;> = <;(b /. n),w;> ) holds
v = w