---

Step * of Lemma reqmatrix_functionality

∀[a,b:ℕ]. ∀[X1,X2,Y1,Y2:ℝ(a × b)].  (uiff(X1 ≡ Y1;X2 ≡ Y2)) supposing (Y1 ≡ Y2 and X1 ≡ X2)
BY
{ (RepUR ``rmatrix reqmatrix`` 0 THEN Auto) }

1
1. a : ℕ
2. b : ℕ
3. X1 : ℕa ⟶ ℕb ⟶ ℝ
4. X2 : ℕa ⟶ ℕb ⟶ ℝ
5. Y1 : ℕa ⟶ ℕb ⟶ ℝ
6. Y2 : ℕa ⟶ ℕb ⟶ ℝ
7. ∀i:ℕa. ∀j:ℕb.  ((X1 i j) = (X2 i j))
8. ∀i:ℕa. ∀j:ℕb.  ((Y1 i j) = (Y2 i j))
9. ∀i:ℕa. ∀j:ℕb.  ((X1 i j) = (Y1 i j))
10. i : ℕa
11. j : ℕb
⊢ (X2 i j) = (Y2 i j)

2
1. a : ℕ
2. b : ℕ
3. X1 : ℕa ⟶ ℕb ⟶ ℝ
4. X2 : ℕa ⟶ ℕb ⟶ ℝ
5. Y1 : ℕa ⟶ ℕb ⟶ ℝ
6. Y2 : ℕa ⟶ ℕb ⟶ ℝ
7. ∀i:ℕa. ∀j:ℕb.  ((X1 i j) = (X2 i j))
8. ∀i:ℕa. ∀j:ℕb.  ((Y1 i j) = (Y2 i j))
9. ∀i:ℕa. ∀j:ℕb.  ((X2 i j) = (Y2 i j))
10. i : ℕa
11. j : ℕb
⊢ (X1 i j) = (Y1 i j)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbN{}].  \mforall{}[X1,X2,Y1,Y2:\mBbbR{}(a  \mtimes{}  b)].    (uiff(X1  \mequiv{}  Y1;X2  \mequiv{}  Y2))  supposing  (Y1  \mequiv{}  Y2  and  X1  \mequiv{}  X2)


By

---

Latex:
(RepUR  ``rmatrix  reqmatrix``  0  THEN  Auto)

---

Home Index