---

Step * 1 1 1 of Lemma mon_nat_op_one


1. g : IMonoid
2. e : |g|
⊢ (e * e) = e ∈ |g|
BY
{ ((RW MonNormC 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  e  :  |g|
\mvdash{}  (e  *  e)  =  e


By

---

Latex:
((RW  MonNormC  0)  THEN  Auto)

---

Home Index