theorem :: ZMODUL02:17

for R being Ring
for V being LeftMod of R
for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by VECTSP_6:12;