---

Step * of Lemma oal_mon_wf

∀a:LOSet. ∀b:AbDMon.  (oal_mon(a;b) ∈ AbDMon)
BY
{ ((UnivCD THENA Auto) THEN ((Unfold `oal_mon` 0) THEN ((BLemma `mk_abdmonoid`) THEN Auto))⋅) }

1
1. a : LOSet@i'
2. b : AbDMon@i'
⊢ IsEqFun(|oal(a;b)|;=b)

2
1. a : LOSet@i'
2. b : AbDMon@i'
⊢ Assoc(|oal(a;b)|;λx,y. (x ++ y))

3
1. a : LOSet@i'
2. b : AbDMon@i'
⊢ Ident(|oal(a;b)|;λx,y. (x ++ y);00)

4
1. a : LOSet@i'
2. b : AbDMon@i'
⊢ Comm(|oal(a;b)|;λx,y. (x ++ y))

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.    (oal\_mon(a;b)  \mmember{}  AbDMon)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  ((Unfold  `oal\_mon`  0)  THEN  ((BLemma  `mk\_abdmonoid`)  THEN  Auto))\mcdot{})

---

Home Index