---

Step * of Lemma fun-connected_transitivity

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

1
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. z : T
6. L1 : T List
7. y=f*(x) via L1
8. L : T List
9. z=f*(y) via L
⊢ ∃L:T List. z=f*(x) via L

---

Latex:

---

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


By

---

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

---

Home Index