---

Step * 1 2 of Lemma ss-fun-fun


1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. [Z] : SeparationSpace
4. λF,p. (F (fst(p)) (snd(p))) ∈ Point(X ⟶ Y ⟶ Z ⟶ X × Y ⟶ Z)
5. λG,x,y. (G <x, y>) ∈ Point(X × Y ⟶ Z ⟶ X ⟶ Y ⟶ Z)
⊢ ss-homeo(X ⟶ Y ⟶ Z;X × Y ⟶ Z)
BY
{ ((D 0 With ⌜λF,p. (F (fst(p)) (snd(p)))⌝  THEN Auto) THEN D 0 With ⌜λG,x,y. (G <x, y>)⌝  THEN Auto THEN RepUR ``ss-ap`\000C` 0) }

1
1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. λF,p. (F (fst(p)) (snd(p))) ∈ Point(X ⟶ Y ⟶ Z ⟶ X × Y ⟶ Z)
5. λG,x,y. (G <x, y>) ∈ Point(X × Y ⟶ Z ⟶ X ⟶ Y ⟶ Z)
6. x : Point(X ⟶ Y ⟶ Z)@i
⊢ λx@0,y. (x x@0 y) ≡ x

2
1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. λF,p. (F (fst(p)) (snd(p))) ∈ Point(X ⟶ Y ⟶ Z ⟶ X × Y ⟶ Z)
5. λG,x,y. (G <x, y>) ∈ Point(X × Y ⟶ Z ⟶ X ⟶ Y ⟶ Z)
6. ∀x:Point(X ⟶ Y ⟶ Z). λG,x,y. (G <x, y>)(λF,p. (F (fst(p)) (snd(p)))(x)) ≡ x
7. y : Point(X × Y ⟶ Z)@i
⊢ λp.(y <fst(p), snd(p)>) ≡ y

---

Latex:

---

Latex:

1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  [Z]  :  SeparationSpace
4.  \mlambda{}F,p.  (F  (fst(p))  (snd(p)))  \mmember{}  Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  \mtimes{}  Y  {}\mrightarrow{}  Z)
5.  \mlambda{}G,x,y.  (G  <x,  y>)  \mmember{}  Point(X  \mtimes{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z)
\mvdash{}  ss-homeo(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z;X  \mtimes{}  Y  {}\mrightarrow{}  Z)


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}F,p.  (F  (fst(p))  (snd(p)))\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}G,x,y.  (G  <x,  y>)\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``ss-ap``  0)

---

Home Index