let R be non degenerated Ring; :: thesis: 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)) #)
let X be non empty set ; :: thesis: 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)) #)
reconsider V = Free_LMod (X,R) as strict LeftMod of R ;
reconsider W = Lin (rng (IotaMap (X,R))) as strict Submodule of V ;
for v being Vector of V holds
( v in W iff v in V ) by Th28;
hence 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)) #) by ZMODUL01:48; :: thesis: verum