theorem ThScFSDM1: :: ZMODLAT3:11

for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for F being FinSequence of (DivisibleMod L)
for v, u being Vector of (DivisibleMod L)
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))