---

Step * of Lemma radd_rcos_wf

∀[x:ℝ]. (radd_rcos(x) ∈ {y:ℝ| y = (x + rcos(x))} )
BY
{ (InstLemma `addrcos_wf2` []
   THEN ParallelLast'
   THEN Unhide
   THEN Unfold `radd_rcos` 0
   THEN Assert ⌜3-regular-seq(addrcos(x))⌝⋅) }

1
.....assertion..... 
1. x : ℝ
2. addrcos(x) ∈ {f:ℕ+ ⟶ ℤ| f = (x + rcos(x))} 
⊢ 3-regular-seq(addrcos(x))

2
1. x : ℝ
2. addrcos(x) ∈ {f:ℕ+ ⟶ ℤ| f = (x + rcos(x))} 
3. 3-regular-seq(addrcos(x))
⊢ accelerate(3;addrcos(x)) ∈ {y:ℝ| y = (x + rcos(x))} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (radd\_rcos(x)  \mmember{}  \{y:\mBbbR{}|  y  =  (x  +  rcos(x))\}  )


By

---

Latex:
(InstLemma  `addrcos\_wf2`  []
  THEN  ParallelLast'
  THEN  Unhide
  THEN  Unfold  `radd\_rcos`  0
  THEN  Assert  \mkleeneopen{}3-regular-seq(addrcos(x))\mkleeneclose{}\mcdot{})

---

Home Index