theorem :: ZMODUL02:16

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