---

Step * of Lemma fix-connected

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f:T ⟶ T].
  ∀[x,y:T].  f**(x) = f**(y) ∈ T supposing x is f*(y) supposing retraction(T;f)
BY
{ xxx(Auto THEN RepeatFor 3 (MoveToConcl (-1)))xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
⊢ ∀x,y:T.  (x is f*(y) ⇒ (f**(x) = f**(y) ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f:T  {}\mrightarrow{}  T].
    \mforall{}[x,y:T].    f**(x)  =  f**(y)  supposing  x  is  f*(y)  supposing  retraction(T;f)


By

---

Latex:
xxx(Auto  THEN  RepeatFor  3  (MoveToConcl  (-1)))xxx

---

Home Index