theorem MATRLIN16: :: ZMODUL05:16
for R being Ring
for V1, V2 being LeftMod of R
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)