theorem Th23: :: RMOD_4:23

for R being Ring
for V being RightMod of R
for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)