---

Step * 2 of Lemma last-event-of-set

.....upcase..... 
1. es : EO@i'
2. n : ℤ@i
3. 0 < n
4. ∀f:ℕn ─→ E. ∃k:ℕn. ∀i:ℕn. f i ≤loc f k  supposing ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)@i
⊢ ∀f:ℕn + 1 ─→ E. ∃k:ℕn + 1. ∀i:ℕn + 1. f i ≤loc f k  supposing ∀i,j:ℕn + 1.  (loc(f i) = loc(f j) ∈ Id)
BY
{ (RepeatFor 2 ((ParallelLast THENA Auto)) THEN ExRepD) }

1
1. es : EO@i'
2. n : ℤ@i
3. 0 < n
4. ∀f:ℕn ─→ E. ∃k:ℕn. ∀i:ℕn. f i ≤loc f k  supposing ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)@i
5. f : ℕn + 1 ─→ E@i
6. ∀i,j:ℕn + 1.  (loc(f i) = loc(f j) ∈ Id)
7. k : ℕn
8. ∀i:ℕn. f i ≤loc f k 
⊢ ∃k:ℕn + 1. ∀i:ℕn + 1. f i ≤loc f k 

---

Latex:


.....upcase..... 
1.  es  :  EO@i'
2.  n  :  \mBbbZ{}@i
3.  0  <  n
4.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  E.  \mexists{}k:\mBbbN{}n.  \mforall{}i:\mBbbN{}n.  f  i  \mleq{}loc  f  k    supposing  \mforall{}i,j:\mBbbN{}n.    (loc(f  i)  =  loc(f  j))@i
\mvdash{}  \mforall{}f:\mBbbN{}n  +  1  {}\mrightarrow{}  E.  \mexists{}k:\mBbbN{}n  +  1.  \mforall{}i:\mBbbN{}n  +  1.  f  i  \mleq{}loc  f  k    supposing  \mforall{}i,j:\mBbbN{}n  +  1.    (loc(f  i)  =  loc(f  j))


By

(RepeatFor  2  ((ParallelLast  THENA  Auto))  THEN  ExRepD)

---

Home Index