---

Step * of Lemma rng_times_zero

∀[r:Rng]. ∀[a:|r|].  (((0 * a) = 0 ∈ |r|) ∧ ((a * 0) = 0 ∈ |r|))
BY
{ ((UnivCD) THENA Auto) }

1
1. r : Rng
2. a : |r|
⊢ ((0 * a) = 0 ∈ |r|) ∧ ((a * 0) = 0 ∈ |r|)

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a:|r|].    (((0  *  a)  =  0)  \mwedge{}  ((a  *  0)  =  0))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index