theorem LMThMBF1X0: :: ZMATRLIN:101

for V being free finite-rank Z_Module
for F being linear-Functional of V
for y being FinSequence of V
for x, X, Y being FinSequence of INT.Ring st X = x & len y = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . (y /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,y)))