theorem :: ZMODUL02:13

for V being Z_Module
for v being VECTOR of V
for F being FinSequence of V
for f being Function of V,INT.Ring
for i being Element of NAT st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v by VECTSP_6:8;