let L be Z_Lattice; :: thesis: 0. (DivisibleMod L) is Dual of L
for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring by LmDE00;
hence 0. (DivisibleMod L) is Dual of L by defDualElement; :: thesis: verum