---

Step * of Lemma strict-fun-connected_transitivity3

∀[T:Type]. ∀f:T ⟶ T. (retraction(T;f) ⇒ (∀x,y,z:T.  (y = f+(x) ⇒ z is f*(y) ⇒ z = f+(x))))
BY
{ (Unfold `strict-fun-connected` 0 THEN Auto) }

1
1. [T] : Type
2. f : T ⟶ T
3. retraction(T;f)
4. x : T
5. y : T
6. z : T
7. ¬(x = y ∈ T)
8. y is f*(x)
9. z is f*(y)
⊢ ¬(x = z ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  (retraction(T;f)  {}\mRightarrow{}  (\mforall{}x,y,z:T.    (y  =  f+(x)  {}\mRightarrow{}  z  is  f*(y)  {}\mRightarrow{}  z  =  f+(x))))


By

---

Latex:
(Unfold  `strict-fun-connected`  0  THEN  Auto)

---

Home Index