let R be comRing; :: thesis: for M being strict LeftMod of R holds AbGrLMod ((AbGr M),(canHom M)) = M
let M be strict LeftMod of R; :: thesis: AbGrLMod ((AbGr M),(canHom M)) = M
AbGrLMod ((AbGr M),(canHom M)) is Submodule of M

proof

set N = AbGrLMod ((AbGr M),(canHom M));
reconsider N = AbGrLMod ((AbGr M),(canHom M)) as LeftMod of R ;
A1: 0. N = 0. M ;
A2: the addF of N = the addF of M || the carrier of N

proof

the addF of N = the addF of M | (dom the addF of M) by RELAT_1:69
.= the addF of M || the carrier of N by FUNCT_2:def 1 ;
hence the addF of N = the addF of M || the carrier of N ; :: thesis: verum

end;

the lmult of N = the lmult of M | [: the carrier of R, the carrier of N:]

proof

dom the lmult of M = [: the carrier of R, the carrier of M:] by FUNCT_2:def 1;
then the lmult of M | [: the carrier of R, the carrier of N:] = the lmult of M by RELAT_1:69
.= the lmult of N by Th35 ;
hence the lmult of N = the lmult of M | [: the carrier of R, the carrier of N:] ; :: thesis: verum

end;

hence AbGrLMod ((AbGr M),(canHom M)) is Submodule of M by A1, A2, VECTSP_4:def 2; :: thesis: verum

end;

hence AbGrLMod ((AbGr M),(canHom M)) = M by VECTSP_4:31; :: thesis: verum