let R be comRing; :: thesis: for M being LeftMod of R holds M ~= AbGrLMod ((AbGr M),(canHom M))
let M be LeftMod of R; :: thesis: M ~= AbGrLMod ((AbGr M),(canHom M))
A1: rho M is Homomorphism of R,M, AbGrLMod ((AbGr M),(canHom M)) by Def10;
( rho M is one-to-one & rho M is onto ) by Th38;
hence M ~= AbGrLMod ((AbGr M),(canHom M)) by A1; :: thesis: verum