let R be non degenerated Ring; :: thesis: for X being non empty set
for N being LeftMod of R
for h being Homomorphism of id R, Free_LMod (X,R),N holds h . (0. (Free_LMod (X,R))) = 0. N
let X be non empty set ; :: thesis: for N being LeftMod of R
for h being Homomorphism of id R, Free_LMod (X,R),N holds h . (0. (Free_LMod (X,R))) = 0. N
let N be LeftMod of R; :: thesis: for h being Homomorphism of id R, Free_LMod (X,R),N holds h . (0. (Free_LMod (X,R))) = 0. N
let h be Homomorphism of id R, Free_LMod (X,R),N; :: thesis: h . (0. (Free_LMod (X,R))) = 0. N
set J = id R;
h . (0. (Free_LMod (X,R))) = h . ((0. R) * (0. (Free_LMod (X,R)))) by VECTSP_1:14
.= ((id R) . (0. R)) * (h . (0. (Free_LMod (X,R)))) by MOD_4:def 17
.= 0. N by VECTSP_1:14 ;
hence h . (0. (Free_LMod (X,R))) = 0. N ; :: thesis: verum