---

Step * of Lemma rng_to_alg_wf

∀R:CRng. (rng_to_alg(R) ∈ algebra{i:l}(R))
BY
{ (D 0 THENA Auto THEN D 1) }

1
1. R : Rng
2. Comm(|R|;*)
⊢ rng_to_alg(R) ∈ algebra{i:l}(R)

---

Latex:

---

Latex:
\mforall{}R:CRng.  (rng\_to\_alg(R)  \mmember{}  algebra\{i:l\}(R))


By

---

Latex:
(D  0  THENA  Auto  THEN  D  1)

---

Home Index