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 holds (Phi v) * (IotaMap (X,R)) = v
let X be non empty set ; :: thesis: for N being LeftMod of R
for v being Function of X, the carrier of N holds (Phi v) * (IotaMap (X,R)) = v
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N holds (Phi v) * (IotaMap (X,R)) = v
let v be Function of X, the carrier of N; :: thesis: (Phi v) * (IotaMap (X,R)) = v
for x being Element of X holds ((Phi v) * (IotaMap (X,R))) . x = v . x

proof

let x be Element of X; :: thesis: ((Phi v) * (IotaMap (X,R))) . x = v . x
((Phi v) * (IotaMap (X,R))) . x = (Phi v) . ((IotaMap (X,R)) . x) by FUNCT_2:15
.= (Phi v) . (Iota (x,R)) by Def19
.= v . x by Th19 ;
hence ((Phi v) * (IotaMap (X,R))) . x = v . x ; :: thesis: verum

end;

hence (Phi v) * (IotaMap (X,R)) = v ; :: thesis: verum