theorem Th22: :: LMODFREE:22

for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)