theorem Th24: :: LMODFREE:25

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 holds (Phi v) * (IotaMap (X,R)) = v