:: deftheorem defScFSDM defines ScFS ZMODLAT3:def 3 :
for L being Z_Lattice
for F being FinSequence of (DivisibleMod L)
for f being Function of (DivisibleMod L),INT.Ring
for v being Vector of (DivisibleMod L)
for b₅ being FinSequence of F_Real holds
( b₅ = ScFS (v,f,F) iff ( len b₅ = len F & ( for i being Nat st i in dom b₅ holds
b₅ . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) ) );