let R be non degenerated Ring; :: thesis: for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R
for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
let X be non empty set ; :: thesis: for N being LeftMod of R
for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R
for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R
for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
let v be Function of X, the carrier of N; :: thesis: for f being Element of (Free_LMod (X,R))
for a being Element of R
for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
let f be Element of (Free_LMod (X,R)); :: thesis: for a being Element of R
for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
let a be Element of R; :: thesis: for x being Element of X holds (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
let x be Element of X; :: thesis: (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x)
(TermFS ((a * f),v)) . x = ((@ (a * f)) . x) * (v . x) by Def28
.= (a * ((@ f) . x)) * (v . x) by Th7
.= a * (((@ f) . x) * (v . x)) by VECTSP_1:def 16
.= a * ((TermFS (f,v)) . x) by Def28 ;
hence (TermFS ((a * f),v)) . x = a * ((TermFS (f,v)) . x) ; :: thesis: verum