theorem LmDE31: :: ZMODLAT3:25

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for i being Nat st i in dom b holds
ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )