---

Step * of Lemma rng_eq_wf

∀[r:RngSig]. (=b ∈ |r| ⟶ |r| ⟶ 𝔹)
BY
{ ModulePiTac 9 ``rng_car rng_eq rng_le rng_plus rng_zero rng_minus rng_times rng_one rng_div`` }

---

Latex:

---

Latex:
\mforall{}[r:RngSig].  (=\msubb{}  \mmember{}  |r|  {}\mrightarrow{}  |r|  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
ModulePiTac  9  ``rng\_car  rng\_eq  rng\_le  rng\_plus  rng\_zero  rng\_minus  rng\_times  rng\_one  rng\_div``

---

Home Index