---

Step * of Lemma permutation-ss-sep

∀[rv,f,g,f',g':Top].  (<f, g> # <f', g'> ~ fun-sep(rv;Point;f;f') ∨ fun-sep(rv;Point;g;g'))
BY
{ (Intros THEN RepUR ``ss-sep permutation-ss set-ss mk-ss`` 0 THEN RepUR ``prod-ss fun-ss mk-ss ss-sep`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv,f,g,f',g':Top].    (<f,  g>  \#  <f',  g'>  \msim{}  fun-sep(rv;Point;f;f')  \mvee{}  fun-sep(rv;Point;g;g'))


By

---

Latex:
(Intros
  THEN  RepUR  ``ss-sep  permutation-ss  set-ss  mk-ss``  0
  THEN  RepUR  ``prod-ss  fun-ss  mk-ss  ss-sep``  0
  THEN  Auto)

---

Home Index