---

Step * of Lemma free-group-generators

∀[X:Type]
  ∀G:Group{i}
    ∀[f,g:MonHom(free-group(X),G)].
      f = g ∈ MonHom(free-group(X),G) supposing ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
BY
{ (Auto THEN (DVar `f' THENA Auto) THEN (DVar `g' THENA Auto) THEN EqTypeCD THEN Auto) }

1
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
⊢ f = g ∈ (|free-group(X)| ⟶ |G|)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}G:Group\{i\}
        \mforall{}[f,g:MonHom(free-group(X),G)].    f  =  g  supposing  \mforall{}x:X.  ((f  free-letter(x))  =  (g  free-letter(x)))


By

---

Latex:
(Auto  THEN  (DVar  `f'  THENA  Auto)  THEN  (DVar  `g'  THENA  Auto)  THEN  EqTypeCD  THEN  Auto)

---

Home Index