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 is Homomorphism of id R, Free_LMod (X,R),N
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 is Homomorphism of id R, Free_LMod (X,R),N
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N holds Phi v is Homomorphism of id R, Free_LMod (X,R),N
let v be Function of X, the carrier of N; :: thesis: Phi v is Homomorphism of id R, Free_LMod (X,R),N
set F = Phi v;
A1: for x, y being Vector of (Free_LMod (X,R)) holds (Phi v) . (x + y) = ((Phi v) . x) + ((Phi v) . y) by Th21;
for a being Scalar of R
for x being Vector of (Free_LMod (X,R)) holds (Phi v) . (a * x) = ((id R) . a) * ((Phi v) . x) by Th22;
hence Phi v is Homomorphism of id R, Free_LMod (X,R),N by A1, MOD_4:def 17; :: thesis: verum