---

Step * of Lemma oal_equal_char

∀a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  (ps = qs ∈ |oal(a;b)| ⇐⇒ ∀u:|a|. ((ps[u]) = (qs[u]) ∈ |b|))
BY
{ ((GenRepD) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. ps : |oal(a;b)|
4. qs : |oal(a;b)|
5. ps = qs ∈ |oal(a;b)|
6. u : |a|
⊢ (ps[u]) = (qs[u]) ∈ |b|

2
1. a : LOSet
2. b : AbDMon
3. ps : |oal(a;b)|
4. qs : |oal(a;b)|
5. ∀u:|a|. ((ps[u]) = (qs[u]) ∈ |b|)
⊢ ps = qs ∈ |oal(a;b)|

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}ps,qs:|oal(a;b)|.    (ps  =  qs  \mLeftarrow{}{}\mRightarrow{}  \mforall{}u:|a|.  ((ps[u])  =  (qs[u])))


By

---

Latex:
((GenRepD)  THENA  Auto)

---

Home Index