---

Step * of Lemma rng_of_alg_wf

∀A:Type. ∀a:algebra_sig{i:l}(A).  (a↓rg ∈ RngSig)
BY
{ Unfolds ``rng_of_alg rng_sig`` 0 THEN Auto⋅ }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}a:algebra\_sig\{i:l\}(A).    (a\mdownarrow{}rg  \mmember{}  RngSig)


By

---

Latex:
Unfolds  ``rng\_of\_alg  rng\_sig``  0  THEN  Auto\mcdot{}

---

Home Index