theorem ThScFSDM6: :: ZMODLAT3:13
for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for F, G being FinSequence of (DivisibleMod L)
for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))