theorem :: ZMODUL02:16

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