let X be non empty set ; :: thesis: for R being non degenerated Ring
for N being LeftMod of R
for f being Element of (Free_LMod (X,R))
for v being Function of X, the carrier of N
for x being Element of X holds PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)
let R be non degenerated Ring; :: thesis: for N being LeftMod of R
for f being Element of (Free_LMod (X,R))
for v being Function of X, the carrier of N
for x being Element of X holds PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)
let N be LeftMod of R; :: thesis: for f being Element of (Free_LMod (X,R))
for v being Function of X, the carrier of N
for x being Element of X holds PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)
let f be Element of (Free_LMod (X,R)); :: thesis: for v being Function of X, the carrier of N
for x being Element of X holds PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)
let v be Function of X, the carrier of N; :: thesis: for x being Element of X holds PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)
let x be Element of X; :: thesis: PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x)
PhiSet (v,f,{.x.}) = (TermFS (f,v)) . x by SETWISEO:17
.= ((@ f) . x) * (v . x) by Def28 ;
hence PhiSet (v,f,{.x.}) = ((@ f) . x) * (v . x) ; :: thesis: verum