---

Step * 2 of Lemma fg-lift_wf

.....set predicate..... 
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
⊢ ∀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:
.....set  predicate..... 
1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
\mvdash{}  \mforall{}x:X.  ((fg-lift(G;f)  free-letter(x))  =  (f  x))


By

---

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

---

Home Index