---

Step * of Lemma mx_wf

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

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[r:RngSig].  \mforall{}[M:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m  {}\mrightarrow{}  |r|].    (matrix(M[x;y])  \mmember{}  Matrix(n;m;r))


By

---

Latex:
(Unfold  `matrix`  0  THEN  ProveWfLemma)

---

Home Index