theorem ZL2ThSc1X: :: ZMODLAT2:62

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
<;v,(b /. n);> = <;w,(b /. n);> ) holds
v = w