for L being Z_Lattice
for v1, v2 being Vector of (DivisibleMod L)
for u1, u2 being Vector of (EMbedding L) st v1 = u1 & v2 = u2 holds
(ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2)