---

Step * 1 1 of Lemma fg-hom_wf


1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. w2 : (X + X) List@i
6. w3 : (X + X) List@i
7. w2 = w3 ∈ ((X + X) List)
⊢ fg-hom(G;f;w2) = fg-hom(G;f;w3) ∈ |G|
BY
{ (RepUR ``fg-hom`` 0 THEN EqCDA THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  w  :  free-word(X)
5.  w2  :  (X  +  X)  List@i
6.  w3  :  (X  +  X)  List@i
7.  w2  =  w3
\mvdash{}  fg-hom(G;f;w2)  =  fg-hom(G;f;w3)


By

---

Latex:
(RepUR  ``fg-hom``  0  THEN  EqCDA  THEN  Auto)

---

Home Index