---

Step * of Lemma mon_nat_op_id

∀[g:IMonoid]. ∀[n:ℕ].  ((n ⋅ e) = e ∈ |g|)
BY
{ ((D 0 THENM D 0) THENA Auto) }

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

---

Latex:

---

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


By

---

Latex:
((D  0  THENM  D  0)  THENA  Auto)

---

Home Index