---

Step * of Lemma ss-fun-fun

No Annotations
∀[X,Y,Z:SeparationSpace].  ss-homeo(X ⟶ Y ⟶ Z;X × Y ⟶ Z)
BY
{ (Auto
   THEN (Assert λF,p. (F (fst(p)) (snd(p))) ∈ Point(X ⟶ Y ⟶ Z ⟶ X × Y ⟶ Z) BY
               ((RWW "ss-fun-point" 0 THENA Auto)
                THEN (MemTypeCD THENA Auto)
                THEN Try (((MemCD THENA Auto) THEN (MemTypeCD THENW Auto)))
                THEN RepUR ``ss-function ss-eq`` 0
                THEN Repeat ((RWW  "ss-fun-point ss-fun-sep prod-ss-point prod-ss-sep" 0 THENA Auto))
                THEN (Auto THEN (D 0 THENA Auto) THEN DSetVars)
                THEN Try (((D -1 THEN D -2 THEN All Reduce) THEN D -4 THEN D 0 With ⌜a1⌝  THEN Auto))
                THEN RepUR ``ss-function`` 5
                THEN D -4
                THEN D -3
                THEN All Reduce
                THEN (InstHyp [⌜x1⌝;⌜x3⌝] 5⋅ THENA (Auto THEN Unfold `ss-eq` 0 THEN ParallelOp -2 THEN Auto))
                THEN (RWO "ss-fun-eq" (-1) THENA Auto)
                THEN (Assert x2 ≡ x4 BY
                            (Unfold `ss-eq` 0 THEN ParallelOp -3 THEN Auto))
                THEN MoveToConcl (-3)
                THEN Fold `not` 0
                THEN Fold `ss-eq` 0
                THEN (InstHyp [⌜x2⌝] (-2)⋅ THENA Auto)
                THEN Unfold `ss-ap` -1
                THEN (Assert ⌜F x3 x2 ≡ F x3 x4⌝⋅ THENM (RelRST THEN Auto))
                THEN (GenConclTerm ⌜F x3⌝⋅ THENA Auto)
                THEN D -2
                THEN Unhide
                THEN Auto))
   ) }

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)
⊢ ss-homeo(X ⟶ Y ⟶ Z;X × Y ⟶ Z)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y,Z:SeparationSpace].    ss-homeo(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z;X  \mtimes{}  Y  {}\mrightarrow{}  Z)


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}F,p.  (F  (fst(p))  (snd(p)))  \mmember{}  Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  \mtimes{}  Y  {}\mrightarrow{}  Z)  BY
                          ((RWW  "ss-fun-point"  0  THENA  Auto)
                            THEN  (MemTypeCD  THENA  Auto)
                            THEN  Try  (((MemCD  THENA  Auto)  THEN  (MemTypeCD  THENW  Auto)))
                            THEN  RepUR  ``ss-function  ss-eq``  0
                            THEN  Repeat  ((RWW    "ss-fun-point  ss-fun-sep  prod-ss-point  prod-ss-sep"  0  THENA  Auto))
                            THEN  (Auto  THEN  (D  0  THENA  Auto)  THEN  DSetVars)
                            THEN  Try  (((D  -1  THEN  D  -2  THEN  All  Reduce)  THEN  D  -4  THEN  D  0  With  \mkleeneopen{}a1\mkleeneclose{}    THEN  Auto))
                            THEN  RepUR  ``ss-function``  5
                            THEN  D  -4
                            THEN  D  -3
                            THEN  All  Reduce
                            THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x3\mkleeneclose{}]  5\mcdot{}
                                        THENA  (Auto  THEN  Unfold  `ss-eq`  0  THEN  ParallelOp  -2  THEN  Auto)
                                        )
                            THEN  (RWO  "ss-fun-eq"  (-1)  THENA  Auto)
                            THEN  (Assert  x2  \mequiv{}  x4  BY
                                                    (Unfold  `ss-eq`  0  THEN  ParallelOp  -3  THEN  Auto))
                            THEN  MoveToConcl  (-3)
                            THEN  Fold  `not`  0
                            THEN  Fold  `ss-eq`  0
                            THEN  (InstHyp  [\mkleeneopen{}x2\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                            THEN  Unfold  `ss-ap`  -1
                            THEN  (Assert  \mkleeneopen{}F  x3  x2  \mequiv{}  F  x3  x4\mkleeneclose{}\mcdot{}  THENM  (RelRST  THEN  Auto))
                            THEN  (GenConclTerm  \mkleeneopen{}F  x3\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Unhide
                            THEN  Auto))
  )

---

Home Index