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