let R be non degenerated Ring; :: thesis: for X being non empty set holds Free_LMod (X,R) is free
let X be non empty set ; :: thesis: Free_LMod (X,R) is free
reconsider S = rng (IotaMap (X,R)) as Subset of (Free_LMod (X,R)) ;
S is base by Th31;
hence Free_LMod (X,R) is free ; :: thesis: verum