theorem :: ZMODUL02:51

for V being Z_Module
for F, G being FinSequence of V
for f being Function of V,INT.Ring holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by VECTSP_6:13;