theorem Th29: :: LMODFREE:30

for R being non degenerated Ring
for X being non empty set holds Lin (rng (IotaMap (X,R))) = ModuleStr(# the carrier of (Free_LMod (X,R)), the addF of (Free_LMod (X,R)), the ZeroF of (Free_LMod (X,R)), the lmult of (Free_LMod (X,R)) #)