theorem :: ZMODLAT2:13

for L being Z_Lattice
for v, u being Vector of (DivisibleMod L)
for a being Element of INT.Ring holds (ScProductDM L) . (v,(a * u)) = a * ((ScProductDM L) . (v,u))