theorem ThScDM6: :: ZMODLAT2:14

for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds
( (ScProductDM L) . ((0. (DivisibleMod L)),v) = 0 & (ScProductDM L) . (v,(0. (DivisibleMod L))) = 0 )