---

Step * of Lemma massoc_imp_unit_diff

∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b:|g|.  ((a ~ b) ⇒ (∃u:|g|. ((g-unit(u)) c∧ (a = (u * b) ∈ |g|))))))
BY
{ UnivCD THENA Auto }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. a ~ b
⊢ ∃u:|g|. ((g-unit(u)) c∧ (a = (u * b) ∈ |g|))

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid
    (Cancel(|g|;|g|;*)  {}\mRightarrow{}  (\mforall{}a,b:|g|.    ((a  \msim{}  b)  {}\mRightarrow{}  (\mexists{}u:|g|.  ((g-unit(u))  c\mwedge{}  (a  =  (u  *  b)))))))


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index