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, g being Element of (Free_LMod (X,R))
for x being Element of X holds (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,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, g being Element of (Free_LMod (X,R))
for x being Element of X holds (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x)
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R))
for x being Element of X holds (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x)
let v be Function of X, the carrier of N; :: thesis: for f, g being Element of (Free_LMod (X,R))
for x being Element of X holds (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x)
let f, g be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X holds (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x)
let x be Element of X; :: thesis: (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x)
(TermFS ((f + g),v)) . x = ((@ (f + g)) . x) * (v . x) by Def28
.= (((@ f) . x) + ((@ g) . x)) * (v . x) by Th8
.= (((@ f) . x) * (v . x)) + (((@ g) . x) * (v . x)) by VECTSP_1:def 15
.= ((TermFS (f,v)) . x) + (((@ g) . x) * (v . x)) by Def28
.= ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x) by Def28 ;
hence (TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x) ; :: thesis: verum