---

Step * 2 1 1 1 of Lemma max-fst-property


1. A : Type@i'
2. T : Type@i'
3. v : T × A@i
4. v1 : T × A@i
5. T ⊆r ℤ@i
6. v = v1 ∈ (ℤ × A)@i
⊢ v = v1 ∈ (T × A)
BY
{ (D 3 THEN D 5)⋅ }

1
1. A : Type@i'
2. T : Type@i'
3. v2 : T@i
4. v3 : A@i
5. v4 : T@i
6. v5 : A@i
7. T ⊆r ℤ@i
8. <v2, v3> = <v4, v5> ∈ (ℤ × A)@i
⊢ <v2, v3> = <v4, v5> ∈ (T × A)

---

Latex:

---

Latex:

1.  A  :  Type@i'
2.  T  :  Type@i'
3.  v  :  T  \mtimes{}  A@i
4.  v1  :  T  \mtimes{}  A@i
5.  T  \msubseteq{}r  \mBbbZ{}@i
6.  v  =  v1@i
\mvdash{}  v  =  v1


By

---

Latex:
(D  3  THEN  D  5)\mcdot{}

---

Home Index