---

Step * of Lemma eo-reset-dom_wf

∀[es:EO]. ∀[d:es-base-E(es) ─→ 𝔹].  (eo-reset-dom(es;d) ∈ EO)
BY
{ (Auto⋅ THEN D 1 THEN MemTypeCD THEN Auto) }

1
1. es : eo_record{i:l}()
2. eo_axioms(es)
3. d : es-base-E(es) ─→ 𝔹
⊢ eo-reset-dom(es;d) ∈ eo_record{i:l}()

2
.....set predicate..... 
1. es : eo_record{i:l}()
2. eo_axioms(es)
3. d : es-base-E(es) ─→ 𝔹
⊢ eo_axioms(eo-reset-dom(es;d))

---

Latex:


\mforall{}[es:EO].  \mforall{}[d:es-base-E(es)  {}\mrightarrow{}  \mBbbB{}].    (eo-reset-dom(es;d)  \mmember{}  EO)


By

(Auto\mcdot{}  THEN  D  1  THEN  MemTypeCD  THEN  Auto)

---

Home Index