theorem LMThMBF1X0: :: ZMODLAT1:90

for V being free finite-rank Z_Module
for F being linear-FrFunctional of V
for y being FinSequence of V
for x being FinSequence of INT.Ring
for X, Y being FinSequence of F_Real 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)))