theorem ThScFS3: :: ZMODLAT3:3

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