theorem ThSc4: :: ZMODLAT1:10

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