theorem :: ZMODUL02:15

for R being Ring
for V being LeftMod of R
for v being VECTOR of V
for f being Function of V,R holds f (#) <*v*> = <*((f . v) * v)*> by VECTSP_6:10;