---

Step * 1 1 1 of Lemma rng_to_alg_wf


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

1
1. R : RngSig
2. IsRing(|R|;+R;0;-R;*;1)
3. Comm(|R|;*)
⊢ rng_to_alg(R) ∈ algebra_sig{i:l}(|R|)

---

Latex:

---

Latex:

1.  R  :  Rng
2.  Comm(|R|;*)
\mvdash{}  rng\_to\_alg(R)  \mmember{}  algebra\_sig\{i:l\}(|R|)


By

---

Latex:
D  1

---

Home Index