theorem LmDE22: :: ZMODLAT2:15

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) = 0 ) holds
for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0