let X be non empty set ; :: thesis: for R being non degenerated Ring
for x being Element of X holds (ev_ (x,R)) . (0. (Free_LMod (X,R))) = 0. R
let R be non degenerated Ring; :: thesis: for x being Element of X holds (ev_ (x,R)) . (0. (Free_LMod (X,R))) = 0. R
let x be Element of X; :: thesis: (ev_ (x,R)) . (0. (Free_LMod (X,R))) = 0. R
(ev_ (x,R)) . (0. (Free_LMod (X,R))) = (@ (0. (Free_LMod (X,R)))) . x by Def20
.= 0. R ;
hence (ev_ (x,R)) . (0. (Free_LMod (X,R))) = 0. R ; :: thesis: verum