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
<;v,u;> = <;w,u;> ) holds
for u being Vector of L holds <;v,u;> = <;w,u;>