---

Step * of Lemma fpf-dom-compose

∀[x:Top]. ∀[f:a:Top fp-> Top]. ∀[g,eq:Top].  (x ∈ dom(g o f) ~ x ∈ dom(f))
BY
{ (Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[x:Top].  \mforall{}[f:a:Top  fp->  Top].  \mforall{}[g,eq:Top].    (x  \mmember{}  dom(g  o  f)  \msim{}  x  \mmember{}  dom(f))


By

(Reduce  0  THEN  Auto)

---

Home Index