---

Step * of Lemma fpf_ap_compose_lemma

∀x,eq,f,g:Top.  (g o f(x) ~ g f(x))
BY
{ (UnivCD THENA Auto) }

1
1. x : Top@i
2. eq : Top@i
3. f : Top@i
4. g : Top@i
⊢ g o f(x) ~ g f(x)

---

Latex:


\mforall{}x,eq,f,g:Top.    (g  o  f(x)  \msim{}  g  f(x))


By

(UnivCD  THENA  Auto)

---

Home Index