theorem ThScFSDM3: :: ZMODLAT3:12

for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>