let M be non empty unital multMagma ; :: thesis: for R being compatible Equivalence_Relation of M holds 1_ (M ./. R) = Class (R,(1_ M))
let R be compatible Equivalence_Relation of M; :: thesis: 1_ (M ./. R) = Class (R,(1_ M))
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 1_ (M ./. R) = Class (R,(1_ M)) by GROUP_1:def 4; :: thesis: verum