---

Step * of Lemma rng_of_alg_wf2

∀a:CRng. ∀m:algebra{i:l}(a).  (m↓rg ∈ Rng)
BY
{ ((RepD) THENA Auto) }

1
1. a : CRng@i'
2. m : algebra{i:l}(a)@i'
⊢ m↓rg ∈ Rng

---

Latex:

---

Latex:
\mforall{}a:CRng.  \mforall{}m:algebra\{i:l\}(a).    (m\mdownarrow{}rg  \mmember{}  Rng)


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index