---

Step * 2 of Lemma rng_times_when_l


1. r : Rng
2. u : |r|
3. v : |r|
⊢ (u * 0) = 0 ∈ |r|
BY
{ ((RW RngNormC 0) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  u  :  |r|
3.  v  :  |r|
\mvdash{}  (u  *  0)  =  0


By

---

Latex:
((RW  RngNormC  0)  THEN  Auto)

---

Home Index