---

Step * of Lemma strict-fun-connected-step

∀[T:Type]. ∀f:T ⟶ T. ∀x:T.  f x = f+(x) supposing ¬((f x) = x ∈ T)
BY
{ xxx(Auto THEN UnfoldTopAb 0⋅ THEN Auto THEN Try (ParallelLast) THEN UnfoldTopAb 0)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x:T.    f  x  =  f+(x)  supposing  \mneg{}((f  x)  =  x)


By

---

Latex:
xxx(Auto  THEN  UnfoldTopAb  0\mcdot{}  THEN  Auto  THEN  Try  (ParallelLast)  THEN  UnfoldTopAb  0)xxx

---

Home Index