theorem Th17: :: ZMATRLIN:17

for V1, V2 being free finite-rank Z_Module
for f being Function of V1,V2
for a being FinSequence of INT.Ring
for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds
f * (lmlt (a,p)) = lmlt (a,(f * p))