theorem Th37: :: ZMATRLIN:32

for V1, V2 being free finite-rank Z_Module
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for a, d being FinSequence of INT.Ring st len a = len b1 holds
for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))