---

Step * of Lemma fun_exp-injection

∀[T:Type]. ∀[f:T ⟶ T].  ∀[n:ℕ]. Inj(T;T;f^n) supposing Inj(T;T;f)
BY
{ (InductionOnNat THEN All (RepUR ``inject``) THEN Auto) }

1
1. T : Type
2. f : T ⟶ T
3. ∀a1,a2:T.  (((f a1) = (f a2) ∈ T) ⇒ (a1 = a2 ∈ T))
4. n : ℤ
5. 0 < n
6. ∀a1,a2:T.  (((f^n - 1 a1) = (f^n - 1 a2) ∈ T) ⇒ (a1 = a2 ∈ T))
7. a1 : T
8. a2 : T
9. (f^n a1) = (f^n a2) ∈ T
⊢ a1 = a2 ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].    \mforall{}[n:\mBbbN{}].  Inj(T;T;f\^{}n)  supposing  Inj(T;T;f)


By

---

Latex:
(InductionOnNat  THEN  All  (RepUR  ``inject``)  THEN  Auto)

---

Home Index