theorem :: LMOD_XX1:8

for M being AbGroup holds End_Ring M is Ring by Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;