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