let M be non empty unital multMagma ; :: thesis: for R being compatible Equivalence_Relation of M
for X, E being Element of (M ./. R) st E = Class (R,(1_ M)) holds
( X * E = X & E * X = X )
let R be compatible Equivalence_Relation of M; :: thesis: for X, E being Element of (M ./. R) st E = Class (R,(1_ M)) holds
( X * E = X & E * X = X )
let X, E be Element of (M ./. R); :: thesis: ( E = Class (R,(1_ M)) implies ( X * E = X & E * X = X ) )
assume A1: E = Class (R,(1_ M)) ; :: thesis: ( X * E = X & E * X = X )
consider x being Element of M such that
A2: X = Class (R,x) by EQREL_1:36;
thus X * E = Class (R,(x * (1_ M))) by A1, A2, Def4
.= X by A2, GROUP_1:def 4 ; :: thesis: E * X = X
thus E * X = Class (R,((1_ M) * x)) by A1, A2, Def4
.= X by A2, GROUP_1:def 4 ; :: thesis: verum