---

Step * of Lemma nat_op_zero

∀[g:IMonoid]. ∀[e:|g|].  (0 x(*;e) e = e ∈ |g|)
BY
{ UnivCD THENA Auto }

1
1. g : IMonoid
2. e : |g|
⊢ 0 x(*;e) e = e ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[e:|g|].    (0  x(*;e)  e  =  e)


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index