reconsider E = Class (R,(1_ M)) as Element of (M ./. R) by EQREL_1:def 3;
for X being Element of (M ./. R) holds
( X * E = X & E * X = X ) by Lm1;
hence M ./. R is unital by GROUP_1:def 1; :: thesis: verum