---

Step * of Lemma fg-hom_wf

∀[X:Type]. ∀[G:Group{i}]. ∀[f:X ⟶ |G|]. ∀[w:free-word(X)].  (fg-hom(G;f;w) ∈ |G|)
BY
{ (Auto THEN Assert ⌜∀w2,w:(X + X) List.  ((λx,y. word-rel(X;x;y)^* w2 w) ⇒ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|))⌝⋅) \000C}

1
.....assertion..... 
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
⊢ ∀w2,w:(X + X) List.  ((λx,y. word-rel(X;x;y)^* w2 w) ⇒ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|))

2
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. ∀w2,w:(X + X) List.  ((λx,y. word-rel(X;x;y)^* w2 w) ⇒ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|))
⊢ fg-hom(G;f;w) ∈ |G|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[G:Group\{i\}].  \mforall{}[f:X  {}\mrightarrow{}  |G|].  \mforall{}[w:free-word(X)].    (fg-hom(G;f;w)  \mmember{}  |G|)


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mforall{}w2,w:(X  +  X)  List.    ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w)  {}\mRightarrow{}  (fg-hom(G;f;w2)  =  fg-hom(G;f;w\000C)))\mkleeneclose{}
            \mcdot{}
  )

---

Home Index