theorem :: ZMODUL01:14

for V being Z_Module
for a being Element of INT.Ring
for v, u being Vector of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)