:: deftheorem defScFS defines ScFS ZMODLAT3:def 1 :
for L being Z_Lattice
for F being FinSequence of L
for f being Function of L,INT.Ring
for v being Vector of 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 = <;v,((f . (F /. i)) * (F /. i));> ) ) );