theorem LmDE32: :: ZMODLAT3:32

for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DualBasis I st v in I holds
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)