---

Step * 1 of Lemma free-group-hom


1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. x : X
⊢ (fg-lift(G;f) free-letter(x)) = (f x) ∈ |G|
BY
{ (RepUR ``fg-lift fg-hom free-letter`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  x  :  X
\mvdash{}  (fg-lift(G;f)  free-letter(x))  =  (f  x)


By

---

Latex:
(RepUR  ``fg-lift  fg-hom  free-letter``  0  THEN  Auto)

---

Home Index