theorem Th18: :: ZMATRLIN:18

for V2, V3 being free finite-rank Z_Module
for g being Function of V2,V3
for b2 being OrdBasis of V2
for a being FinSequence of INT.Ring st len a = len b2 & g is additive & g is homogeneous holds
g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))