---

Step * of Lemma mon_nat_op_one

∀[g:IMonoid]. ∀[e:|g|].  ((1 ⋅ e) = e ∈ |g|)
BY
{ ((UnivCD) THENA Auto) }

1
1. g : IMonoid
2. e : |g|
⊢ (1 ⋅ e) = e ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[e:|g|].    ((1  \mcdot{}  e)  =  e)


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index