---

Step * of Lemma posint_mul_mon_wf

<ℤ+,*> ∈ AbMon
BY
{ ((Unfold `posint_mul_mon` 0 THEN BLemma `mk_abmonoid`) THENA Auto) }

1
Assoc(ℕ+;λx,y. (x * y))

2
Ident(ℕ+;λx,y. (x * y);1)

3
Comm(ℕ+;λx,y. (x * y))

---

Latex:

---

Latex:
<\mBbbZ{}\msupplus{},*>  \mmember{}  AbMon


By

---

Latex:
((Unfold  `posint\_mul\_mon`  0  THEN  BLemma  `mk\_abmonoid`)  THENA  Auto)

---

Home Index