theorem ZL2ThSc1D: :: ZMODLAT2:63

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