---

Step * of Lemma munit_of_op

∀g:IAbMonoid. ∀a,b:|g|.  ((g-unit(a * b)) ⇒ ((g-unit(a)) ∧ (g-unit(b))))
BY
{ ((GenUnivCD) THENA Auto) }

1
1. g : IAbMonoid
2. a : |g|
3. b : |g|
4. g-unit(a * b)
⊢ g-unit(a)

2
1. g : IAbMonoid
2. a : |g|
3. b : |g|
4. g-unit(a * b)
⊢ g-unit(b)

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}a,b:|g|.    ((g-unit(a  *  b))  {}\mRightarrow{}  ((g-unit(a))  \mwedge{}  (g-unit(b))))


By

---

Latex:
((GenUnivCD)  THENA  Auto)

---

Home Index