---

Step * 1 of Lemma reqmatrix_functionality


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)
BY
{ (RWW "-5< -4< -3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  X1  :  \mBbbN{}a  {}\mrightarrow{}  \mBbbN{}b  {}\mrightarrow{}  \mBbbR{}
4.  X2  :  \mBbbN{}a  {}\mrightarrow{}  \mBbbN{}b  {}\mrightarrow{}  \mBbbR{}
5.  Y1  :  \mBbbN{}a  {}\mrightarrow{}  \mBbbN{}b  {}\mrightarrow{}  \mBbbR{}
6.  Y2  :  \mBbbN{}a  {}\mrightarrow{}  \mBbbN{}b  {}\mrightarrow{}  \mBbbR{}
7.  \mforall{}i:\mBbbN{}a.  \mforall{}j:\mBbbN{}b.    ((X1  i  j)  =  (X2  i  j))
8.  \mforall{}i:\mBbbN{}a.  \mforall{}j:\mBbbN{}b.    ((Y1  i  j)  =  (Y2  i  j))
9.  \mforall{}i:\mBbbN{}a.  \mforall{}j:\mBbbN{}b.    ((X1  i  j)  =  (Y1  i  j))
10.  i  :  \mBbbN{}a
11.  j  :  \mBbbN{}b
\mvdash{}  (X2  i  j)  =  (Y2  i  j)


By

---

Latex:
(RWW  "-5<  -4<  -3"  0  THEN  Auto)

---

Home Index