theorem :: ZMATRLIN:100

for V being free finite-rank Z_Module
for i being Nat
for a1 being Element of INT.Ring
for a2 being Element of V
for p1 being FinSequence of INT.Ring
for p2 being FinSequence of V st i in dom (lmlt (p1,p2)) & a1 = p1 . i & a2 = p2 . i holds
(lmlt (p1,p2)) . i = a1 * a2 by FUNCOP_1:22;