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 x being Element of X holds (Phi v) . (Iota (x,R)) = 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 x being Element of X holds (Phi v) . (Iota (x,R)) = v . x
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N
for x being Element of X holds (Phi v) . (Iota (x,R)) = v . x
let v be Function of X, the carrier of N; :: thesis: for x being Element of X holds (Phi v) . (Iota (x,R)) = v . x
let x be Element of X; :: thesis: (Phi v) . (Iota (x,R)) = v . x
set fx = Iota (x,R);
SuppFin (Iota (x,R)) = {.x.} by Lm16;
then (Phi v) . (Iota (x,R)) = PhiSet (v,(Iota (x,R)),{.x.}) by Def31;
then (Phi v) . (Iota (x,R)) = ((@ (Iota (x,R))) . x) * (v . x) by Th17
.= (1. R) * (v . x) by Def17
.= v . x ;
hence (Phi v) . (Iota (x,R)) = v . x ; :: thesis: verum