theorem :: ZMODUL02:14

for V being Z_Module
for f being Function of V,INT.Ring holds f (#) (<*> the carrier of V) = <*> the carrier of V by VECTSP_6:9;