theorem :: ZMODUL02:13

for R being Ring
for V being LeftMod of R
for v being VECTOR of V
for F being FinSequence of V
for f being Function of V,R
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;