theorem :: ZMODUL02:15

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