theorem Th19: :: LMODFREE:19

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 x being Element of X holds (Phi v) . (Iota (x,R)) = v . x