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 x being Element of X st not x in Support (@ f) holds
(TermFS (f,v)) . x = 0. N
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 x being Element of X st not x in Support (@ f) holds
(TermFS (f,v)) . x = 0. N
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 x being Element of X st not x in Support (@ f) holds
(TermFS (f,v)) . x = 0. N
let v be Function of X, the carrier of N; :: thesis: for f being Element of (Free_LMod (X,R))
for x being Element of X st not x in Support (@ f) holds
(TermFS (f,v)) . x = 0. N
let f be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X st not x in Support (@ f) holds
(TermFS (f,v)) . x = 0. N
let x be Element of X; :: thesis: ( not x in Support (@ f) implies (TermFS (f,v)) . x = 0. N )
assume not x in Support (@ f) ; :: thesis: (TermFS (f,v)) . x = 0. N
then (@ f) . x = 0. R by POLYNOM1:def 4;
hence (TermFS (f,v)) . x = (0. R) * (v . x) by Def28
.= 0. N by VECTSP_1:14 ;
:: thesis: verum