Step * of Lemma fpf-dom-compose

[x:Top]. ∀[f:a:Top fp-> Top]. ∀[g,eq:Top].  (x ∈ dom(g f) x ∈ dom(f))
BY
(Reduce 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