theorem Th16: :: ZMATRLIN:16

for V1, V2 being Z_Module
for f being Function of V1,V2
for p being FinSequence of V1 st f is additive & f is homogeneous holds
f . (Sum p) = Sum (f * p)