---

Step * of Lemma matrix-ap_wf

∀[n,m:ℤ]. ∀[r:RngSig]. ∀[i:ℕn]. ∀[j:ℕm]. ∀[M:Matrix(n;m;r)].  (M[i,j] ∈ |r|)
BY
{ (Unfold `matrix` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[r:RngSig].  \mforall{}[i:\mBbbN{}n].  \mforall{}[j:\mBbbN{}m].  \mforall{}[M:Matrix(n;m;r)].    (M[i,j]  \mmember{}  |r|)


By

---

Latex:
(Unfold  `matrix`  0  THEN  ProveWfLemma)

---

Home Index