theorem ThSc3: :: ZMODLAT1:9

for L being Z_Lattice
for v, u being Vector of L
for a being Element of INT.Ring holds <;v,(a * u);> = a * <;v,u;>