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