for R being Ring
for V being RightMod of R
for F, G being FinSequence of V
for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)